Quentin Carbonneaux comments

Repositories
Issues
Comments

Results 4 comments of


                                            Quentin Carbonneaux

HOL-Light with recent versions of ocaml & camlp5 ?

I just opened PR #74 that might be of interest.

HOL-Light with recent versions of ocaml & camlp5 ?

I can confirm that it works. I recently setup an opam switch from scratch for ocaml 4.14.1, then run `make` and got a working `hol.sh`. Good job @aqjune, HOL-Light is...

Working ocaml-camlp5 pairs

Would it be possible to run `holtest` instead of simply loading the prelude? That may be too resource-consuming, so maybe a lighter version of holtest can be adapted.

No release - and none with OCaml 5 support

Thanks a lot @aqjune for all the work you put into democratizing this lovely proof system.