Open Casteran opened 9 months ago
Looks to be an issue specific to Latex output generation.
The html
file generated by the same snippet is OK w.r.t. the display of local definitions x:= A: t
, whilst they appear as x: t
in the pdf
document.
I didn't test the other output formats.
Cc: @cpitclaudel
Here is a simpler example:
(* begin snippet LProof *)
Lemma L: exists z: bool, negb z = true.
Proof.
pose (z := false).
exists z.
(* error in latex output : *)
reflexivity.
Qed.
(* end snippet LProof *)
On the html output, the goal just before reflexivity
is correctly displayed.
On the latex/pdf output, this goal is printed as:
z: bool
===========
negb z = true
Which is clearly unsolvable.
This issue seems to be solved if one replaces in latex.py
the method gen_hyp
with
def gen_hyp(self, hyp):
names = self.gen_names(hyp.names)
hbody = [self.gen_code(hyp.body)] if hyp.body else []
with macros.hyp(args=[names], optargs=hbody, verbatim=True):
self.gen_code(hyp.type)
if hyp.body != None:
self.gen_txt(r":= ")
self.gen_code(hyp.body)
self.gen_txt(r" ")
self.gen_mrefs(hyp)
This change has been tested successfully on the hydra-battles book. Could someone have a look and improve the python code ? Being a Python beginner, I didn't dare to open a PR with poor style.
Nevertheless, it would be fine to fix this issue before the next release.
In the following proof,
alectryon AlectryonIssue.v --backend latex
builds a document where the variablez
is presented as a simple declarationz: nat
and notz := Nat.max x y : nat
, which makes the displayed sub-goals apparently unsolvable.Indeed, the displayed sub-goal
is unsolvable, but if the definition
z := max x y: nat
were displayed, the generated doc would be OK.I noticed this issue only in Latex output mode. My alectryon version is Alectryon v1.5.0-dev
Note: this issue occurs also in the CI of hydra-battles on the top of page 227 of the doc (file https://github.com/coq-community/hydra-battles/blob/master/theories/ordinals/MoreAck/AckNotPR.v ).