search

Deducteam / Logipedia

An encyclopedia of proofs
56 stars 11 forks source link

Pretty printer #14

Open gabrielhdt opened 4 years ago

gabrielhdt commented 4 years ago

Could the binary of the pretty printer be passed as an argument of logigen? For instance, one would use logigen -i json/ -o web --pp /usr/bin/ppt. By default, the json object could be printed (although it's not pretty).

rprimet commented 4 years ago

Yep the pretty-printer could be an option, especially if we have 2+ choices, but I'd rather have a good default (otherwise the CLI might become tedious to use).

gabrielhdt commented 4 years ago

So you want the pretty printer to be in the repository?

rprimet commented 4 years ago

No, not at all (it might be a separate package, or it might live in the repository at the start, whichever you prefer) -- I just want to have a default executable name to call it. (logipedia-pp or similar?)

De: "Gabriel Hondet" notifications@github.com À: "Deducteam/Logipedia" Logipedia@noreply.github.com Cc: "Romain Primet" romain.primet@inria.fr, "Comment" comment@noreply.github.com Envoyé: Jeudi 17 Octobre 2019 13:35:58 Objet: Re: [Deducteam/Logipedia] Pretty printer (#14)

So you want the pretty printer to be in the repository?

— You are receiving this because you commented. Reply to this email directly, [ https://github.com/Deducteam/Logipedia/issues/14?email_source=notifications&email_token=ACO7RM2WUCM2VIBKHOJUBQTQPBEZ5A5CNFSM4JBUZNIKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEBPY3EY#issuecomment-543133075 | view it on GitHub ] , or [ https://github.com/notifications/unsubscribe-auth/ACO7RM2ZZSNDZ422HWZXC5DQPBEZ5ANCNFSM4JBUZNIA | unsubscribe ] .

rprimet commented 4 years ago

Come to think of it, being able to set the pretty-printer executable through an environment variable (e.g LOGIPEDIA_PP or similar) might also be a good choice (but then we need to define a priority order...)

gabrielhdt commented 4 years ago

Ah all right, that's a good idea. I think we should

  1. use an environment variable
  2. use the command line flag

so that if both are set, the command line flag is taken into account. Why not logipedia-pp or logipp, take the one you prefer. I have already some prototypes at logippedia.