Unable to get cargo hax into coq working #1484
Description
Example
I'm trying to get the example from the website working.
Below is a sequence of commands which basically shows everything
$ cat src/main.rs
fn main() { square_requires(15); }
#[hax_lib::requires(x < 16)]
fn square_requires(x: u8) -> u8 { x * x }
$ cargo hax into coq
Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.02s
info: hax: wrote file ./proofs/coq/extraction/Sample.v
info: hax: wrote file ./proofs/coq/extraction/_CoqProject
$ cd proofs/coq/extraction; coq_makefile -f _CoqProject -o Makefile
$ make
COQDEP VFILES
COQC Sample.v
File "./Sample.v", line 2, characters 0-31:
Warning:
Use of "( _ | _ )" Notation is deprecated as it is inconsistent with pattern syntax.
[disj-pattern-notation,syntax]
File "./Sample.v", line 12, characters 0-30:
Warning: Notation "LIST_CONS" was already used.
[notation-overridden,parsing,default]
File "./Sample.v", line 18, characters 40-44:
Error: Unbound and ungeneralizable variable f_lt.
make[1]: *** [Sample.vo] Error 1
make: *** [all] Error 2
Info
I'm on a macbook with an M1 pro.
$ opam switch
# switch compiler description
-> 5.1.1 ocaml-base-compiler.5.1.1,ocaml-options-vanilla.1 ocaml-base-compiler = 5.1.1 | ocaml-system = 5.1.1
default ocaml-base-compiler.5.2.0,ocaml-options-vanilla.1 ocaml >= 4.05.0
$ coqc -v
The Coq Proof Assistant, version 8.18.0
compiled with OCaml 5.1.1
$ cargo hax -V
hax untagged-git-rev-b4692fc54c
Any help appreciated! I'm doing this for my bachelor's thesis and would really like to get it working.