Hiding proof completely

[jjhugues]

Hi,

I am using Alectryon to document a large development with the objective to generate a PDF document. I could navigate docutils to generate LaTeX files from each .v file the way I want.

I miss the ability to hide completely proofs.

Some are relevant and should be documented, but I have many well-formedness rules for which I need to show the definition, but hide the trivial proofs. Is there an option to do so ? Basically I want to suppress the block starting from Proof. to Qed.

Thanks,

[cpitclaudel]

There's a few ways to do this. You can use a .. coq:: none marker before the proof block, but that's invasive; or, you could use a custom griver to recognize ( Proof …. Qed ) blocks

[jjhugues]

coq:: none works, but I was thinking of something similar in (usage) to fold/unfold, e.g. a hide or suppress keyword to suppress the proof would meet my need.

What do you mean by 'griver' in the context of alectryon?

[cpitclaudel]

What do you mean by 'griver' in the context of alectryon?

Apparently I can neither type nor proofread ^^ I meant "driver", sorry. And by that I meant that you could have a custom keyword that you'd attach to "Proof" and that would hide everything until Qed.

[jjhugues]

Hi,

Thanks, I thought griver (like grive in French) was some kind of wordplay about birds from the Coq community again ;)

Ideally, I would want this to hide all proofs. This is less intrusive

(*| .. coq:: no-proof |*)

Lemma basics : 1 + 1 = 2.
Proof.
  trivial.
Qed.

If I understood your proposition, you would have instead for each proof:

Lemma basics : 1 + 1 = 2.
Proof. (* no-proof *)
  trivial.
Qed.

This is easier said than done though. The main issue I have is in understanding the code base to inject the right behavior.

For the first approach, I could hack into docutils.py around line 670 (__aply or replaceio* functions) to detect the "Proof" sentence, apply the annotation for all subsequent sentences until the "Qed" sentence is read.

For the second one, I am lost: I would need a similar approach in an external tool that would preprocess the reST input and do the same text removal. This would mean injecting a specific step in alectryon pipelines.

What would you suggest?

[cpitclaudel]

Happy to help, but I'm drowning in work right now. Is it OK if I get back to you in a few days? (Most likely not before the end of the week, but please ping me after that)

[jjhugues]

Thanks, a few days or weeks is perfect.

[cpitclaudel]

Thanks a lot. Please ping me in a week or two if I don't resurface until then.

[jjhugues]

Hi @cpitclaudel , hope you found the surface again! If you can get me started on this one, I could probably work out some details.