Build failure with Coq 8.18
I downloaded the repository and ran make
, and that failed:
COQDEP VFILES
CAMLDEP diaframe/ocaml/ltac2_extra.mli
OCAMLLIBDEP diaframe/ocaml/diaframe_plugin.mlpack
CAMLDEP diaframe/ocaml/ltac2_extra.ml
COQDEP TESTFILES
*** Warning: in file supplements/diaframe_heap_lang_examples/wip/k42_alt.v, library k42_lock is required from root diaframe.heap_lang.examples.wip and has not been found in the loadpath!
*** Warning: in file tutorial/ex3_xchg_refinements.v, library proof_automation is required from root diaframe.reloc and has not been found in the loadpath!
*** Warning: in file tutorial/ex4_xchg_logatom.v, library proof_automation is required from root diaframe.reloc and has not been found in the loadpath!
*** Warning: in file tutorial/ex4_xchg_logatom.v, library symb_exec_logatom is required from root diaframe.reloc and has not been found in the loadpath!
CAMLC -c diaframe/ocaml/ltac2_extra.mli
COQC diaframe/util_classes.v
COQC diaframe/env_utils.v
COQC diaframe/lib/own/proofmode_classes.v
CAMLOPT -c -for-pack Diaframe_plugin diaframe/ocaml/ltac2_extra.ml
File "diaframe/ocaml/ltac2_extra.ml", line 13, characters 40-60:
13 | Tac2env.define_primitive (pname name) (mk_closure arity f)
^^^^^^^^^^^^^^^^^^^^
Error: This expression has type Value.closure = Ltac2_plugin.Tac2ffi.closure
but an expression was expected of type Ltac2_plugin.Tac2ffi.valexpr
make: *** [CoqMakefile:757: diaframe/ocaml/ltac2_extra.cmx] Error 2
COQC diaframe/steps/namer_tacs.v
COQC diaframe/lib/own/proofmode_instances.v
File "./diaframe/lib/own/proofmode_instances.v", line 948, characters 8-50:
Error: Anomaly "conversion was given unreduced term (FLambda)."
Please report at http://coq.inria.fr/bugs/.
make: *** [CoqMakefile:838: diaframe/lib/own/proofmode_instances.vo] Error 129
make: *** [diaframe/lib/own/proofmode_instances.vo] Deleting file 'diaframe/lib/own/proofmode_instances.glob'
make: Target 'default' not remade because of errors.
$ coqc --version
The Coq Proof Assistant, version 8.18.0
compiled with OCaml 4.14.0