Skip to content
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

Inconsistent use of hash_id in TheoryFolder class #316

Open
wdcraft01 opened this issue Nov 2, 2023 · 0 comments
Open

Inconsistent use of hash_id in TheoryFolder class #316

wdcraft01 opened this issue Nov 2, 2023 · 0 comments
Assignees
Labels

Comments

@wdcraft01
Copy link
Collaborator

In working on database-related stuff in the TheoryFolder and TheoryFolderStorage classes, we discovered an inconsistency in the use of object hash_ids in the name_to_hash.txt files and in the subsequent processing of axiom and theorem nbs when an axiom or theorem name is modified without modifications to the actual content (expression) of the axiom or theorem. This arises because the name_to_hash.txt files are currently using the hash_id associated with the entire object (which hash_id is then also incorporating the name of an axiom or theorem), and thus a change of name is also changing the hash_id being used to track the content of the axiom or theorem object .... In any case, after some discussion and review of some example cases, @wwitzel has recommended we edit the related methods (mostly the TheoryFolder._set_special_objects() and TheoryFolder._load_special_names() methods) to enact the use of expression hash ids (instead of higher-level object hash ids) in the name_to_hash.txt files and related code.
Addressing this issue might also end up addressing some very occasionally-occurring bug where a theorem proof is lost or misplaced in the process of renaming a theorem.

@wdcraft01 wdcraft01 added the bug label Nov 2, 2023
@wdcraft01 wdcraft01 self-assigned this Nov 2, 2023
wdcraft01 added a commit that referenced this issue Nov 18, 2023
Related Issue: #316 . In setting/getting/loading special objects (common expressions, axioms, theorems) and special object names, shift from using object hash ids to expression hash ids. This entails shifting the TheoryFolder dictionary _special_hash_ids to _special_expr_ids, and also shifting the TheoryFolder dictionary _kindname_to_objhash to _kindname_to_exprhash, with subsequent changes throughout the TheoryFolder class and some fewer changes in the TheoryFolderStorage class. These changes are intended to allow better (and more accurately informative) handling of situations in which special object names are changed without changes to the content/definition of the special object (and vice-versa). These changes do not affect the database folders (an axiom, for example, is still 'stored' in a folder labeled with its obj hash id), but these changes effectively replace the name_to_hash.txt files with name_to_expr_id.txt files.
wdcraft01 added a commit that referenced this issue Nov 18, 2023
Related Issue: #316 . This notebook can soon be deleted, but currently serves to help check system performance when we import some 'special objects' (common expression, axiom, theorem) before and after a special object is re-named.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant