-
Notifications
You must be signed in to change notification settings - Fork 139
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Remaining issues of HOL's OpenTheory packaging #805
Comments
NOTE: point 3 seems not true: HOL's OpenTheory reader can indeed replay proofs stored in OpenTheory articles. |
Copied from PR #1022:
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 Move subtopology theorems from real_topology to (general) topology #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
The text was updated successfully, but these errors were encountered: