metaprl's People
metaprl's Issues
Theory saving and exporting issues
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.
-
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. -
After running
check_all()
orstatus_all()
, all the related theory saves theirprlb
files, while there's not changes are made (from the user) at all. I guess this behavior is due to version mismatch? -
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 upprlb
files and rebuild them from the newprla
generated. I guess it is the also due to version mismatch.
Build error
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.
test13 in Itt_int_test
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.
What is bug 256?
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?
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.