Commit 29951767 authored by POTTIER Francois's avatar POTTIER Francois

Added a link to CompCert's Parser.vy.

parent 53d6057e
......@@ -1946,10 +1946,14 @@ in \texttt{.vy} and generates a Coq file whose name ends
in \texttt{.v}.
Like a \texttt{.mly} file, a \texttt{.vy} file is a grammar specification,
with embedded semantic actions. The main difference is that the semantic
with embedded semantic actions. The only difference is that the semantic
actions in a \texttt{.vy} file are expressed in Coq instead
of \ocaml. A \texttt{.vy} file otherwise uses the same syntax as
a \texttt{.mly} file. There are however several restrictions:
a \texttt{.mly} file. CompCert's
\href{https://github.com/AbsInt/CompCert/tree/master/cparser/Parser.vy}{\texttt{Parser.vy}}
serves as an example.
Several restrictions are imposed when \menhir is used in \ocoq mode:
%
\begin{itemize}
\item The error handling mechanism (\sref{sec:errors}) is absent.
......@@ -2074,7 +2078,7 @@ named \verb+unambiguous+.
The parsers produced by \menhir's Coq back-end must be linked with a Coq
library, which can be found in the CompCert tree~\cite{compcert,compcert-github}, in the
\href{https://github.com/AbsInt/CompCert/tree/master/cparser/validator}
{\texttt{cparser/validator}} subdirectory. Additionally, CompCert can be used as
{\texttt{cparser/validator}} subdirectory. CompCert can be used as
an example if one wishes to use \menhir to generate a formally verified parser
as part of some other project.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment