search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
630 stars 142 forks source link

Fix otknl build #1338

Closed binghe closed 1 week ago

binghe commented 1 week ago

Hi,

This should fix the otknl build. There's only one small shift of goals in the generated "hol4-assums.art" causing failure when building src/boss/prove_base_assumsTheory. The previous th62 is now th60 (th62 |-> th60; th60 |-> th61; th61 |-> th62), very local changes, perhaps due to modifications in listTheory.

Let's see how the CI goes.

--Chun

binghe commented 1 week ago

The way to fix such issues is to evaluate expressions like el 60 goals |> concl at the broken theorem, and check if the output matches the theorem statements in near comments (that I added just for this purpose), and if not the same, the current proof is not for the current goal (but another goal in different place). Only in rare cases we need to add whole new proofs to handle more goals (currently there are 96 of them).

mn200 commented 1 week ago

Thanks for getting this done!