Pierre Rousselin (Sep 25 2023 at 08:39): Pierre Rousselin (Sep 25 2023 at 08:39):My little "initiation to formal proofs" course will start tomorrow. It's not completely necessary, but I was wondering if there is a simple solution to lock most tactics and then unlock them progressively. For instance at the beginning to only allow intros apply and exact.
Théo Zimmermann (Sep 25 2023 at 09:06):That's a long-wanted feature, and I don't think there is any simple way of doing this.
Théo Zimmermann (Sep 25 2023 at 09:07):One could probably come up with an alternative Prelude / Ltac plugin that would do this, but it would probably represent significant work.
Pierre Rousselin (Sep 25 2023 at 09:09):Thank you for your answer, if I think of a solution, I will share it.
Théo Zimmermann (Sep 25 2023 at 09:10):Actually, if you just want to forbid a precise list of tactics, I can think of a solution. You can override them by defining a Tactic Notation that fails.
Théo Zimmermann (Sep 25 2023 at 09:14):Very basic example:
Tactic Notation "apply" constr(x) := fail "Unauthorized".
Goal True.
apply I. (* Tactic failure: Unauthorized. *)
Yes, that's a good solution (and it's probably possible and worth it to write these for all tactics and then unlock a very small subset). But then I would have to hide these in some way in order not to pollute too much the file (or give them in a separate file to require, but then we're back to compilation issues or other problems if jscoq is used)
Théo Zimmermann (Sep 25 2023 at 09:21):Oh indeed, you would have to distribute a library. That's probably overkill for your use case, but the best way to distribute a precompiled library to students is probably to create a custom Coq Platform (cf. https://github.com/coq/platform/blob/main/doc/FAQ-customized-installers.md).
Pierre Rousselin (Sep 25 2023 at 09:24):Thanks, I will think about it for later (not tomorrow !).
Side remark, the fact that a --dangerous option exists and that it's actually used, made me smile :
snap install --dangerous coq-prover_2022-09-0_amd64.snap
Another way would be to implement a coq-lsp / fleche / fcc linter plugin that errors on those
Emilio Jesús Gallego Arias (Sep 25 2023 at 11:26):People used SerAPI to do similar stuff, but the new API we offer in Flèche is way more convenient to use
Pierre Rousselin (Sep 26 2023 at 14:19):I think I will try this eventually.
Last updated: Oct 13 2024 at 01:02 UTC