What is the EvalOp in Coq CompCert

Question

The definition of EvalOp is in compcert.backend.SplitLongproof:

Ltac EvalOp :=
  eauto;
  match goal with
  | [ |- eval_exprlist _ _ _ _ _ Enil _ ] => constructor
  | [ |- eval_exprlist _ _ _ _ _ (_:::_) _ ] => econstructor; EvalOp
  | [ |- eval_expr _ _ _ _ _ (Eletvar _) _ ] => constructor; simpl; eauto
  | [ |- eval_expr _ _ _ _ _ (Elet _ _) _ ] => econstructor; EvalOp
  | [ |- eval_expr _ _ _ _ _ (lift _) _ ] => apply eval_lift; EvalOp
  | [ |- eval_expr _ _ _ _ _ _ _ ] => eapply eval_Eop; [EvalOp | simpl; eauto]
  | _ => idtac
  end.

What is strange about this definition is that coqdoc --html recognize Eval and Op as two separate tokens:

<span class="id" title="keyword">Eval</span><span class="id" title="var">Op</span>

Why would Coq allow two tokens with no separators (spaces) in the middle? Or is this a bug of coqdoc? Thanks for helping!

[Here](http://compcert.inria.fr/doc/html/SplitLongproof.html) I see `EvalOp`. — Anton Trunov, Mar 26 '18 at 21:59
@AntonTrunov I compiled CompCert and the doc using coq 8.7.1+2 in opam. My doc command is `coqdoc --html -q -R lib compcert.lib -R common compcert.common -R x86_64 compcert.x86_64 -R x86 compcert.x86 -R backend compcert.backend -R cfrontend compcert.cfrontend -R driver compcert.driver -R flocq compcert.flocq -R exportclight compcert.exportclight -R cparser compcert.cparser --vernac-file lib/*.v common/*.v x86_64/*.v x86/*.v backend/*.v cfrontend/*.v driver/*.v flocq/*.v exportclight/*.v cparser/*.v` Do you know how the official doc is compiled, and why this bug happens on my machine? — Jian Wang, Mar 26 '18 at 22:06
@AntonTrunov Or could it be because there is a bug in compcert 3.2 while the bug was resolved in the compcert master version? — Jian Wang, Mar 26 '18 at 22:07
I don't know, but could it be an instance of [issue #2366](https://github.com/coq/coq/issues/2366)? — Anton Trunov, Mar 26 '18 at 22:12
Also, could it be that CompCert uses [coq2html](https://github.com/xavierleroy/coq2html) instead of coqdoc to generate HTML? — Anton Trunov, Mar 26 '18 at 22:15
@AntonTrunov I see, so it is likely a bug in `coqdoc --html`. I would like to try the solution of issue #2366 (`cd theories && coqdoc -toc -html -d html *.v`), but how does it applies to the case where the v files are in multiple folders? For example, If I run `coqdoc` once for each folders in compcert, I guess I will lose the variable `href` links for the variables defined in different folders? — Jian Wang, Mar 26 '18 at 22:22
Sorry, I don't know. I either use generated coqdoc files or just browse/grep the source code. — Anton Trunov, Mar 26 '18 at 22:56
`Eval` being a vernacular token, I think it's just some tool in the chain being confused about the proper tokenization. :-( — Ptival, Mar 27 '18 at 01:00
@Ptival Do you think the bug is in the Coq parser? Does `coqdoc` use the same parser as `coqc` does? If yes, is `coqc` safe in this case? — Jian Wang, Mar 28 '18 at 00:24
Last I checked, `coqdoc` and `coqc` used separate parsers. In any case, `coqc` does not have this issue. — Jason Gross, May 10 '18 at 00:44

score 3 · Accepted Answer · answered May 10 '18 at 00:50

Why would Coq allow two tokens with no separators (spaces) in the middle? Or is this a bug of coqdoc?

This is a bug of coqdoc. Coq does not allow two alphabetic tokens with no non-alphanumeric characters between them, but there are plenty of other examples of tokens without separators. For example, this is valid Coq:

Definition(*no-spaces*)foo:=1.

This gets lexed as the tokens Definition, the comment (*no-spaces*), foo, :=, 1, and ., I believe. You can also play silly games with numeric tokens, e.g.,

Coercion Nat.add:nat>->Funclass.
Axiom a:nat.
Check 1a:nat.

Because identifiers cannot start with numbers, Coq parses 1a as 1 applied to a, which typechecks because of the Coercion. You should probably not play games like this with Coq's parser.

What is the EvalOp in Coq CompCert

1 Answers1