Theory saving and exporting issues

[LdBeth]

After get the system running I'm already able to check the theory, even have proved some simple examples, at the same time I have also experienced some problems.

1. There seems no way to cache proof status of theorems, every time starting MetaPRL requires running check_all(), although I know that NuPRL 5 has similar problem, and MetaPRL is already thousands times faster than NuPRL, I still expect to have cache features like Agda.

2. After running check_all() or status_all(), all the related theory saves their prlb files, while there's not changes are made (from the user) at all. I guess this behavior is due to version mismatch?

3. I think the prla exporting feature is a nice one since it provides certain form of check point, but I have face certain failures that exporting causes inconsistency between theories that causes certain theories fail to be open again. It is some times required to clean up prlb files and rebuild them from the new prla generated. I guess it is the also due to version mismatch.

[LdBeth]

I just made a workaround solving reporting

Invalid Argument:
       Filter_summary.dest_id: not an int

when trying to build a exported prla ASCII IO file. https://github.com/owo-lang/metaprl/commit/28de493cbff4152376c75fd818eaa71f3c691efc

but it is still kinda abnormal for a large number like this occurs in exported file:

theories/itt/core/itt_void.prla
1063:P  p14 Number 1636726926

Since all numbers in the old exported files are all relatively small.

@ANogin

[ANogin]

1. Why would you want to cache status for everything? You can run expand_all in a specific theory you care about, or check_all if you want it recursively.

2. Yes, probably. But prlb should only be saved when you ask MetaPRL to save, not automatically.

3. There should not be issues with version mismatch, provided you update the version numbers in filter/base/filter_magic.ml when you make any changes that would cause the types of prlb/cmoz/cmiz to change (or just delete all the cmoz/cmiz/prlb files when you are messing with these things locally with no danger of causing problems for somebody else with your changes) - this way it knows which binary files are incompatible and will automatically do the right thing. Your dest_id issue might be caused by it trying to unmarshall an incompatible type, and so you get garbage somewhere.

[LdBeth]

Your dest_id issue might be caused by it trying to unmarshall an incompatible type, and so you get garbage somewhere.

I try to understand the format of ASCII IO, and find that these to terms are probably related, the first from the original file and the second from my exported prla file:

NSummary!id id  id Summary
P   p1123   Number 577314270
O   o1123   id p1123

NSummary!id     id      id Summary
P       p14     Number 1636726926
O       o14     id p14

Some other files such as itt_union has similar things happened.

I guess it is some kind of timestamp or checksum, and it just happened that it overflows, since the int size set in libmojave is fairly small.

[LdBeth]

I figured out that this number is indeed generated by the hash function in filter_cache_fun.ml, and affected by the available OCaml word size. I think I'd just rather not worry about it.

[ANogin]

The point is that the OCaml type is int. If you have this not fitting into an int, that means you have created a .prla from an incompatible misinterpreted binary (that is, binary created with marshalling one OCaml type and loaded by unmarshalling with another) which needed to be prevented by properly updating filter/base/filter_magic.ml version number. The dest_id is just a symptom - your .prla is potentially corrupted and who knows what else is wrong and how else it will affect you...

[LdBeth]

Yes, I've checked that the new checksum (1636726926 and 2000480577 are all 31-bit) is still in the 62-bit range that OCaml int type has on x86_64 machine. It is just that Lm_num.is_integer_num from jyh/libmojave actually has no knowledge about the int size of OCaml, but assumes int size to be 15+15=30 bit, which is apparently too small for today's machine, where MetaPRL's hash function does take advantage of 64 bit machine, thus causes this bug. Since the with the modified libmojave the checksum mechanism does not report any problems, I'd assume there's no other bugs corrupts the prla file, and mark this as the fix.