search

Deducteam / Logipedia

An encyclopedia of proofs
56 stars 11 forks source link

provide a flag to choose output system(s) #5

Closed rprimet closed 4 years ago

rprimet commented 5 years ago

In the export code, it may be useful to be able to configure / choose output systems at run time. This may help provide quicker checks especially as most time seems to be spent in the exporter for a single system (opentheory).

gabrielhdt commented 4 years ago

Currently, there is one make target per system. Assuming make coq has been run, coq files are lying in export/coq. Generating json only using coq files is simply a matter of logipedia json --coq export/coq -o export/json -f path/to/file.dk.

Do you need more?

rprimet commented 4 years ago

LGTM, I don't think we need more!