jyh / metaprl Goto Github PK

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.

I have the following build error:

File "macro_main.ml", line 1, characters 0-12:
Error: Unbound module Odyl_main

It is probably configuration issue with OMake, but unfortunately I don't know OMake at all. camlp5 is installed and "-I" points to the correct directory.

I'm playing with the tests in theories/itt/tests to make sure I didn't create trouble when replace the naive big_int based Lm_num with Zarith (there's a comment in itt_omega writes that Lm_num didn't play well with the hash function because equal numbers have different representations, but Zarith can ensure hash function produce same results on equal numbers). And omegaT can pass all tests in itt_int_test except test13, which is:

interactive test13 :
	sequent { <H> >- 'a in int } -->
	sequent { <H>; 'a >= 0;
                  1 >= 5 *@ 'a
                  >- "assert"{bfalse} }

?[1,6] rule test13 :
    <Γ> ⊢ a ∈ int ──→
    <Γ>; a≥0; (5 * a)≤1 ⊢ ↑false

This seems cannot be proved because when take a=0, the formula a≥0 and (5 * a)≤1 are both satisfied, thus False cannot be derived. It is strange that seems no one had noticed it or added a comment about it.

I see it is mentioned several times among comments in filter directory. I think it is time to migrate to CamlP5 8.00 and if I'd like to know if there's any chance this CamlP5 related bug can be resolved during this migration since the rewriting of filter_ocaml is necessary anyway.

* XXX: TODO: This converts the old-style location data into the modern one.
* Ideally, we should be able to embed location data as comments (bug 256).

Unfortunately the original bugzilla seems unavailable now and I didn't get any luck from archive.org either. It is hard for me to be sure about what the proposed "comment" concept is.

 * XXX: TODO: Once comments on terms or soft abstractions are implemented (bugs 256/261),
 *            the "le"/"gt" forms should have a comment that makes sure they will be displayed
 *            as "le"/"gt".

I do know what soft abstraction is from NuPRL, so I just made a bold guess that there will be a new slot added to opname that will record these additional properties, which is opaque to the refiner but visible to other utils like dform?

@ANogin @jyh