search

mortberg / cubicaltt

Experimental implementation of Cubical Type Theory
https://arxiv.org/abs/1611.02108
MIT License
571 stars 76 forks source link

Add command-line options to run commands (or take a command file) and/or redirect output #103

Closed favonia closed 2 years ago

favonia commented 6 years ago

This will simplify the batch job description a lot!

guillaumebrunerie commented 6 years ago

Could you give examples of what you mean? I’m thinking that for instance we could have a command

:n>big.txt u

to redirect the normal form of u in the file big.txt rather than printing it. Are you thinking of something else?

favonia commented 6 years ago

I want something with absolutely zero interaction. For example, a line such as

./cubical -t examples/brunerie.ctt -e brunerie -e another_lemma -o output.txt

is good (syntax inspired by many other interpreters). Output redirection is optional, but taking inputs from the command lines (or -c input.txt from some file) will help a lot.

guillaumebrunerie commented 6 years ago

Ah, makes sense, I can take a look.

guillaumebrunerie commented 6 years ago

The -e option is now implemented (commit fedeb45), but not yet -o. You can now run

cubical examples/brunerie.ctt -e brunerie -e another_lemma

and it will load the file, run all the lemmas that you gave as a -e, then exit. If you want normal forms, the syntax is cubical file.ctt -e ":n lemma".

Note also that the option -t does not exist anymore (it’s now always on).

favonia commented 6 years ago

Is there anyone working on the option -o now?

mortberg commented 6 years ago

I don't think so...

favonia commented 2 years ago

Closing this due to lack of interest.