search

jonsterling / JonPRL

An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]
http://www.jonprl.org
MIT License
109 stars 9 forks source link

Importing libraries #226

Closed vrahli closed 9 years ago

vrahli commented 9 years ago

It would be great if there was a way to import other files from a .jonprl file.

jonsterling commented 9 years ago

This is done using .cfg files (like in Twelf). So, rather than importing a file from within a file, instead you simply place the two files in the same development "configuration", as follows:

sources.cfg: 

my-file1.jonprl
myfile2.jonprl

Then, if you run jonprl sources.cfg, the entire development will be checked. An example of this in action is located in examples/foundations/sources.cfg. If you update to the latest version of the emacs mode, there is support for using cfg files.

We don't yet have namespacing or access control, so this is all a bit fiddly at the moment, but I'm hoping to improve that stuff in the future.

vrahli commented 9 years ago

Great! I looks like "/"s are not allowed in cfg files. I don't seem to be able to import foundations/prelude.jonprl from the example directory.

On Thu, Sep 3, 2015 at 3:40 PM, Jonathan Sterling notifications@github.com wrote:

This is done using .cfg files (like in Twelf). So, rather than importing a file from within a file, instead you simply place the two files in the same development "configuration", as follows:

sources.cfg:

my-file1.jonprl myfile2.jonprl

Then, if you run jonprl sources.cfg, the entire development will be checked. An example of this in action is located in examples/foundations/sources.cfg. If you update to the latest version of the emacs mode, there is support for using cfg files.

We don't yet have namespacing or access control, so this is all a bit fiddly at the moment, but I'm hoping to improve that stuff in the future.

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/JonPRL/issues/226#issuecomment-137449284.

http://www.cs.cornell.edu/~rahli/

jonsterling commented 9 years ago

Ok; I've opened #229, and will fix it ASAP.

jonsterling commented 9 years ago

@vrahli When you get a chance, can you see if the latest version fixes this problem?

vrahli commented 9 years ago

Works fine now.