Prove-It icon indicating copy to clipboard operation
Prove-It copied to clipboard

Inconsistent use of hash_id in TheoryFolder class

Open wdcraft01 opened this issue 2 years ago • 0 comments
trafficstars

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 avatar Nov 02 '23 21:11 wdcraft01