search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

2.0.6 won't build with ocaml-4.08.1 #123

Closed Ponce closed 4 years ago

Ponce commented 4 years ago

platform: Slackware x86_64 ocaml-4.08.1 ocaml-findlib-1.8.1

ocamlbuild -classic-display -no-links src/abella.native
/usr/bin/ocamlopt.opt unix.cmxa -I /usr/lib64/ocaml/ocamlbuild /usr/lib64/ocaml/ocamlbuild/ocamlbuildlib.cmxa myocamlbuild.ml /usr/lib64/ocaml/ocamlbuild/ocamlbuild.cmx -o myocamlbuild
Recreating "src/version.ml"
ocamlfind ocamldep -modules src/abella.ml > src/abella.ml.depends
ocamlfind ocamldep -modules src/abella_types.ml > src/abella_types.ml.depends
ocamlfind ocamldep -modules src/extensions.ml > src/extensions.ml.depends
ocamlfind ocamldep -modules src/metaterm.ml > src/metaterm.ml.depends
ocamlfind ocamldep -modules src/context.ml > src/context.ml.depends
ocamlfind ocamlc -c -bin-annot -strict-formats -w @a-4-29-40-41-42-44-45-48-58-59-60 -I src -I test/ext -o src/extensions.cmo src/extensions.ml
ocamlfind ocamldep -modules src/term.mli > src/term.mli.depends
ocamlfind ocamldep -modules src/pretty.mli > src/pretty.mli.depends
ocamlfind ocamlc -c -bin-annot -strict-formats -w @a-4-29-40-41-42-44-45-48-58-59-60 -I src -I test/ext -o src/pretty.cmi src/pretty.mli
ocamlfind ocamldep -modules src/unify.mli > src/unify.mli.depends
ocamlfind ocamldep -modules src/subordination.mli > src/subordination.mli.depends
ocamlfind ocamlc -c -bin-annot -strict-formats -w @a-4-29-40-41-42-44-45-48-58-59-60 -I src -I test/ext -o src/term.cmi src/term.mli
ocamlfind ocamlc -c -bin-annot -strict-formats -w @a-4-29-40-41-42-44-45-48-58-59-60 -I src -I test/ext -o src/subordination.cmi src/subordination.mli
ocamlfind ocamlc -c -bin-annot -strict-formats -w @a-4-29-40-41-42-44-45-48-58-59-60 -I src -I test/ext -o src/unify.cmi src/unify.mli
ocamlfind ocamldep -modules src/state.mli > src/state.mli.depends
ocamlfind ocamlc -c -bin-annot -strict-formats -w @a-4-29-40-41-42-44-45-48-58-59-60 -I src -I test/ext -o src/context.cmo src/context.ml
ocamlfind ocamlc -c -bin-annot -strict-formats -w @a-4-29-40-41-42-44-45-48-58-59-60 -I src -I test/ext -o src/state.cmi src/state.mli
ocamlfind ocamldep -modules src/typing.ml > src/typing.ml.depends
ocamlfind ocamlc -c -bin-annot -strict-formats -w @a-4-29-40-41-42-44-45-48-58-59-60 -I src -I test/ext -o src/metaterm.cmo src/metaterm.ml
+ ocamlfind ocamlc -c -bin-annot -strict-formats -w @a-4-29-40-41-42-44-45-48-58-59-60 -I src -I test/ext -o src/metaterm.cmo src/metaterm.ml
File "src/metaterm.ml", line 254, characters 46-64:
254 |                  List.fast_sort (fun n1 n2 -> Pervasives.compare (term_head_name n1) (term_head_name n2))
                                                    ^^^^^^^^^^^^^^^^^^
Error (alert deprecated): module Stdlib.Pervasives
Use Stdlib instead.

If you need to stay compatible with OCaml < 4.07, you can use the 
stdlib-shims library: https://github.com/ocaml/stdlib-shims
Command exited with code 2.
make: *** [Makefile:7: all] Error 10
Cleaning up...
chaudhuri commented 4 years ago

Yes, OCaml made a backwards incompatible change to their API in 4.08 by getting rid of the Pervasives module. Since as of now there isn't a reliable fix that works for both pre and post 4.08 versions (without patch files), we will revisit this once Debian testing moves to 4.08 before making a bugfix release. However, I will try to change master to remove all explicit appeals to Pervasives.

chaudhuri commented 4 years ago

Fixed by merging #125