diff -Nru hol-light-20190729/debian/changelog hol-light-20190729/debian/changelog --- hol-light-20190729/debian/changelog 2019-12-29 12:24:09.000000000 +0000 +++ hol-light-20190729/debian/changelog 2020-02-21 01:31:39.000000000 +0000 @@ -1,3 +1,16 @@ +hol-light (20190729-4build1) focal; urgency=medium + + * No change rebuild against new ocaml ABI + + -- Dimitri John Ledkov Fri, 21 Feb 2020 01:31:39 +0000 + +hol-light (20190729-4) unstable; urgency=medium + + * Team upload + * Fix compilation with camlp5 7.11 + + -- Stéphane Glondu Wed, 12 Feb 2020 05:43:48 +0100 + hol-light (20190729-3) unstable; urgency=medium * Team upload diff -Nru hol-light-20190729/debian/control hol-light-20190729/debian/control --- hol-light-20190729/debian/control 2019-12-29 12:24:09.000000000 +0000 +++ hol-light-20190729/debian/control 2020-02-21 01:31:39.000000000 +0000 @@ -1,15 +1,16 @@ Source: hol-light Section: math Priority: optional -Maintainer: Debian OCaml Maintainers +Maintainer: Ubuntu Developers +XSBC-Original-Maintainer: Debian OCaml Maintainers Uploaders: Hendrik Tews Build-Depends: - camlp5 (>= 7.01), + debhelper-compat (= 12), + camlp5 (>= 7.11), ocaml-base-nox, libnum-ocaml-dev, - dh-ocaml (>= 0.9~), - debhelper-compat (= 12) + dh-ocaml Standards-Version: 4.4.1 Rules-Requires-Root: no Homepage: http://www.cl.cam.ac.uk/~jrh13/hol-light/ diff -Nru hol-light-20190729/debian/patches/0004-Fix-compilation-with-camlp5-7.11.patch hol-light-20190729/debian/patches/0004-Fix-compilation-with-camlp5-7.11.patch --- hol-light-20190729/debian/patches/0004-Fix-compilation-with-camlp5-7.11.patch 1970-01-01 00:00:00.000000000 +0000 +++ hol-light-20190729/debian/patches/0004-Fix-compilation-with-camlp5-7.11.patch 2020-02-12 04:43:48.000000000 +0000 @@ -0,0 +1,66 @@ +From: Stephane Glondu +Date: Wed, 12 Feb 2020 05:42:32 +0100 +Subject: Fix compilation with camlp5 7.11 + +--- + pa_j_4.xx_7.xx.ml | 17 +++++++++++------ + 1 file changed, 11 insertions(+), 6 deletions(-) + +diff --git a/pa_j_4.xx_7.xx.ml b/pa_j_4.xx_7.xx.ml +index 4f7ed60..e834058 100755 +--- a/pa_j_4.xx_7.xx.ml ++++ b/pa_j_4.xx_7.xx.ml +@@ -410,9 +410,10 @@ and reloc_module_type floc sh = + | MtApp loc x1 x2 → + let loc = floc loc in + MtApp loc (self x1) (self x2) +- | MtFun loc x1 x2 x3 → ++ | MtFun loc x x3 → + let loc = floc loc in +- MtFun loc x1 (self x2) (self x3) ++ let x = vala_map (option_map (fun (x1, x2) -> (x1, self x2))) x in ++ MtFun loc x (self x3) + | MtLid loc x1 → + let loc = floc loc in + MtLid loc x1 +@@ -507,9 +508,10 @@ and reloc_module_expr floc sh = + | MeApp loc x1 x2 → + let loc = floc loc in + MeApp loc (self x1) (self x2) +- | MeFun loc x1 x2 x3 → ++ | MeFun loc x x3 → + let loc = floc loc in +- MeFun loc x1 (reloc_module_type floc sh x2) (self x3) ++ let x = vala_map (option_map (fun (x1, x2) -> (x1, reloc_module_type floc sh x2))) x in ++ MeFun loc x (self x3) + | MeStr loc x1 → + let loc = floc loc in + MeStr loc (vala_map (List.map (reloc_str_item floc sh)) x1) +@@ -2007,7 +2009,7 @@ EXTEND + | -> <:vala< [] >> ] ] + ; + mod_binding: +- [ [ i = V UIDENT; me = mod_fun_binding -> (i, me) ] ] ++ [ [ i = V uidopt "uidopt"; me = mod_fun_binding -> (i, me) ] ] + ; + mod_fun_binding: + [ RIGHTA +@@ -2070,7 +2072,7 @@ EXTEND + <:sig_item< value $lid:i$ : $t$ >> ] ] + ; + mod_decl_binding: +- [ [ i = V UIDENT; mt = module_declaration -> (i, mt) ] ] ++ [ [ i = V uidopt "uidopt"; mt = module_declaration -> (i, mt) ] ] + ; + module_declaration: + [ RIGHTA +@@ -2092,6 +2094,9 @@ EXTEND + | "module"; i = V mod_ident ""; ":="; me = module_expr -> + <:with_constr< module $_:i$ := $me$ >> ] ] + ; ++ uidopt: ++ [ [ m = V UIDENT -> Some m ] ] ++ ; + (* Core expressions *) + expr: + [ "top" RIGHTA diff -Nru hol-light-20190729/debian/patches/cd-holtest-parallel.patch hol-light-20190729/debian/patches/cd-holtest-parallel.patch --- hol-light-20190729/debian/patches/cd-holtest-parallel.patch 2019-12-29 12:24:09.000000000 +0000 +++ hol-light-20190729/debian/patches/cd-holtest-parallel.patch 2020-02-12 04:43:48.000000000 +0000 @@ -1,5 +1,13 @@ -Description: cd for holtest_parallel because it works only in that directory -Author: Hendrik Tews +From: Hendrik Tews +Date: Wed, 12 Feb 2020 05:41:25 +0100 +Subject: cd for holtest_parallel because it works only in that directory + +--- + holtest_parallel | 2 ++ + 1 file changed, 2 insertions(+) + +diff --git a/holtest_parallel b/holtest_parallel +index 4d462a3..365fed5 100755 --- a/holtest_parallel +++ b/holtest_parallel @@ -20,6 +20,8 @@ diff -Nru hol-light-20190729/debian/patches/default-hollight-dir hol-light-20190729/debian/patches/default-hollight-dir --- hol-light-20190729/debian/patches/default-hollight-dir 2019-12-29 12:24:09.000000000 +0000 +++ hol-light-20190729/debian/patches/default-hollight-dir 2020-02-12 04:43:48.000000000 +0000 @@ -1,5 +1,13 @@ -Description: configure default HOL Light source directory -Author: Hendrik Tews +From: Hendrik Tews +Date: Wed, 12 Feb 2020 05:41:25 +0100 +Subject: configure default HOL Light source directory + +--- + hol.ml | 10 +++++++++- + 1 file changed, 9 insertions(+), 1 deletion(-) + +diff --git a/hol.ml b/hol.ml +index 5af34f7..e319bd2 100644 --- a/hol.ml +++ b/hol.ml @@ -11,10 +11,18 @@ diff -Nru hol-light-20190729/debian/patches/holtest-no-proof-recording.patch hol-light-20190729/debian/patches/holtest-no-proof-recording.patch --- hol-light-20190729/debian/patches/holtest-no-proof-recording.patch 2019-12-29 12:24:09.000000000 +0000 +++ hol-light-20190729/debian/patches/holtest-no-proof-recording.patch 2020-02-12 04:43:48.000000000 +0000 @@ -1,8 +1,16 @@ -Description: don't build the proof-recording version as part of the test suite -Author: Hendrik Tews +From: Hendrik Tews +Date: Wed, 12 Feb 2020 05:41:25 +0100 +Subject: don't build the proof-recording version as part of the test suite + +--- + holtest | 8 ++++---- + 1 file changed, 4 insertions(+), 4 deletions(-) + +diff --git a/holtest b/holtest +index 086b40b..d5043ef 100755 --- a/holtest +++ b/holtest -@@ -205,7 +205,7 @@ +@@ -205,7 +205,7 @@ echo '### Loading 100/two_squares.ml'; echo 'loadt "100/two_squares.ml";;' | (ti echo '### Loading 100/wilson.ml'; echo 'loadt "100/wilson.ml";;' | (time $hollight) # Build the proof-recording version of HOL diff -Nru hol-light-20190729/debian/patches/series hol-light-20190729/debian/patches/series --- hol-light-20190729/debian/patches/series 2019-12-29 12:24:09.000000000 +0000 +++ hol-light-20190729/debian/patches/series 2020-02-12 04:43:48.000000000 +0000 @@ -1,3 +1,4 @@ default-hollight-dir holtest-no-proof-recording.patch cd-holtest-parallel.patch +0004-Fix-compilation-with-camlp5-7.11.patch