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

[favonia]

This will simplify the batch job description a lot!

[guillaumebrunerie]

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]

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]

Ah, makes sense, I can take a look.

[guillaumebrunerie]

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]

Is there anyone working on the option -o now?

[mortberg]

I don't think so...

[favonia]

Closing this due to lack of interest.