Open binghe opened 4 years ago
src/coalgebras/ltree.art
cannot be converted to ltree.ot.art
. See https://github.com/HOL-Theorem-Prover/HOL/pull/958#issuecomment-950878372 for more details.NOTE: point 3 seems not true: HOL's OpenTheory reader can indeed replay proofs stored in OpenTheory articles.
Copied from PR #1022:
ordinalTheory
now contain workarounds for the definition of ordDIV
and ordMOD
as described already. If OpenTheory (or the exporting code in HOL) gets fixed in the future, my current workaround should be reverted.option_case_eq'
in optionTheory
must have been already proved somewhere but I just cannot find it in HOL's core theory proofs. Perhaps it's actually inside a library?src/opentheory/compat
there are some sample HOL theories to try to import bool
and other packages from OT and turn it into a valid HOL theory with proofs. So far I only fixed obvious mistakes due to SML structure name changes.set
and HOL's pred_set
. There are some related mapping calls in pred_setScript.sml
but I think currently all such calls do not work at all.
Following PR #803, I found the following remaining issues in OpenTheory packaging:
itself
type inboolTheory
introduced some new type, constant and theorems. When these theorems are used in other core theories, they become external constants and extra assumptions in the OpenTheory package, because thehol-base
package doesn't packageboolTheory
at all, instead it tries to reuse what OpenTheory's ownbase
package has, with a minimal fake bool theory defined insrc/boss/bool_defsScript.sml
. This mechanism can be seen insrc/boss/hol4-base.thy
:I think it's better to not touch
boolTheory
any more, and move the existingitself
type to other core theory files likeoneTheory
(as they're quite similar), which will be packaged as is. But, if one really wants to add new theorems inboolTheory
, to maintain the OpenTheory compatibility, we need to also updatesrc/boss/prove_base_assumsScript.sml
adding the same theorem in.Some HOL theories (e.g.
real_topologyTheory
) are too big to generate.ot.art
files within limited memory (e.g. 16GB). This is also one reason that I file PR #804 to move some theorems out ofreal_topologyTheory
.I think HOL's OpenTheory reader (now at
src/opentheory/reader/OpenTheoryReader.sml
) is not a fully functional reader: it doesn't actually replay the proof steps stored in.art
files, because the loaded theorems all have special tags (MK_THM
?) with them. Currently it only reads out the theorem statements in*.art
files.--Chun