Juneyoung Lee

Fix tactics in impconv.ml to raise Failure rather than Unchanged

1

Tactics in impconv.ml may raise `Unchanged` rather than `Failure` if they fail. This makes `ORELSE` unable to use because `ORELSE` only catches `Failure` but not `Unchanged`: ``` # g `1...

This patch supports compilation of HOL Light. If the `HOLLIGHT_USE_MODULE` environment variable is set to 1, Makefile builds `hol_lib.cmo` and makes `hol.sh` to use it. It first generates `hol_lib_inlined.ml` which...

This patch adds support for checkpointing HOL Light using DMTCP. It adds a new `make-checkpoint.sh` which uses DMTCP to build a binary. Usage example: ``` make-checkpoint.sh ~/my-checkpoint.sh # Checkpoints HOL...

https://github.com/leanprover/lean4/blob/082c65f22691b7e65158afd8fc8e8358527ae65c/src/Init/Data/BitVec/Basic.lean#L292-L295 In these lines, `-9` is out of bounds of a bit-vector with 4 bits. If `#4` means something else, it must be clarified.

This patch - Fixes TacticTrace to support OCaml 5.4 - Add an example to TacticTrace. This can be checked with `make test` inside TacticTrace dir, as well as `make -f...

Add var type consistency check to e(tac)

2

This patch adds a small but useful check to `e(tac)`: detecting seemingly identical variables that in fact have different types. ``` # g `f (x:num) = f 1`;; Warning: inventing...

It would be great if HOL Light's continuous integration monthly checks whether there is any discrepancy between the expected output of examples in Help/*.hlp and their actual output. A question...