<commit_before>\chapter{Theory Realizations}
\label{chap:realizations}

Given a \why theory, one can use a proof assistant to make a
\emph{realization} of this theory, that is to provide definitions for
some of its uninterpreted symbols and proofs for some of its
axioms. This way, one can show the consistency of an axiomatized
theory and/or make a connection to an existing library (of the proof
assistant) to ease some proofs.
Currently, realizations are supported only for the proof assistant Coq.
% Currently, realizations are supported for the proof assistants Coq and PVS.

\section{Generating a realization}

Generating the skeleton for a theory is done by passing to \why the
\verb+--realize+ option, a driver suitable for realizations, the names of
the theories to realize, and a target directory.

\begin{verbatim}
why3 --realize -D path/to/drivers/prover-realize.drv
      -T env_path.theory_name -o path/to/target/dir/
\end{verbatim}
The name of the generated file is inferred from the theory name. If the
target directory already contains a file with the same name, \why
extracts all the parts that it assumes to be user-edited and merges them in
the generated file.

Note that \why does not track dependencies between realizations and
theories, so a realization will become outdated if the corresponding
theory is modified.
It is up to the user to handle such dependencies, for instance using a
\texttt{Makefile}.

\section{Using realizations inside proofs}

If a theory has been realized, the \why printer for the corresponding prover
will no longer output declarations for that theory but instead simply put
a directive to load the realization. In order to tell the printer
that a given theory is realized, one has to add a meta declaration in the
corresponding theory section of the driver.
\begin{verbatim}
theory env_path.theory_name
  meta "realized" "env_path.theory_name", "optional_naming"
end
\end{verbatim}
The first parameter is the theory name for \why, while the second
parameter, if not empty, provides a name to be used inside generated
scripts to point to the realization, in case the default name is not
suitable for the interactive prover.

\section{Generated/edited files}

\subsection{Coq}

This section describes the content of the Coq files generated by \why for
both proof obligations and theory realizations. When reading a Coq
script, \why is guided by the presence of empty lines to split the
script, so the user should refrain from removing empty lines around
generated parts or adding empty lines inside them.

\begin{enumerate}
\item	The header of the file contains all the library inclusions
	required by the driver file. Any user-made changes to this part
	will be lost when the file is regenerated by \why. This part ends
	at the first empty line.
\item	Abstract logic symbols are assumed with the vernacular directive
	\verb+Paramater+. Axioms are assumed with the \verb+Axiom+
	directive. When regenerating a script, \why assumes that all such
	symbols have been generated by a previous run. As a consequence,
	the user should not introduce new symbols with these two
	directives, as they would be lost.
\item	Definitions of functions and inductive types in theories are
	printed in a block that starts with \verb+(* Why3 assumption *)+.
	This comment should not be removed; otherwise \why will assume
	that the definition is user-made.
\item	Finally, proof obligations and symbols to be realized are
	introduced by \verb+(* Why3 goal *)+. The user is supposed to
	fill the script after the statement. \why assumes that the
	user-made part extends up to \verb+Qed+, \verb+Admitted+,
	\verb+Save+, or \verb+Defined+, whichever comes first. In the
	case of definitions, the original statement can be replaced by
	a \verb+Notation+ directive, in order to ease the usage of
	already defined symbols.
\end{enumerate}

Currently, the parser for Coq scripts is rather naive and does not know
much about comments. For instance, \why can easily be confused by
some terminating directive like \verb+Qed+ that would be present in a
comment.

\input{./pvs.tex}

\section{Shipping libraries of realizations}

While modifying an existing driver file might be sufficient for local
use, it does not scale well when the realizations are to be shipped to
other users. Instead, an additional configuration file should be created.

\begin{verbatim}
[main]
loadpath="path/to/theories"

[prover coq]
option="-R path/to/vo/files Logical_directory"
driver="path/to/extra_coq.drv"
\end{verbatim}

This file can be passed to \why thanks to the \verb+--extra-config+
option.


%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:<commit_msg>Update documentation on Coq realizations.<commit_after>\chapter{Theory Realizations}
\label{chap:realizations}

Given a \why theory, one can use a proof assistant to make a
\emph{realization} of this theory, that is to provide definitions for
some of its uninterpreted symbols and proofs for some of its
axioms. This way, one can show the consistency of an axiomatized
theory and/or make a connection to an existing library (of the proof
assistant) to ease some proofs.
Currently, realizations are supported for the proof assistants Coq and PVS.

\section{Generating a realization}

Generating the skeleton for a theory is done by passing to \why the
\verb+--realize+ option, a driver suitable for realizations, the names of
the theories to realize, and a target directory.

\begin{verbatim}
why3 --realize -D path/to/drivers/prover-realize.drv
      -T env_path.theory_name -o path/to/target/dir/
\end{verbatim}
The name of the generated file is inferred from the theory name. If the
target directory already contains a file with the same name, \why
extracts all the parts that it assumes to be user-edited and merges them in
the generated file.

Note that \why does not track dependencies between realizations and
theories, so a realization will become outdated if the corresponding
theory is modified.
It is up to the user to handle such dependencies, for instance using a
\texttt{Makefile}.

\section{Using realizations inside proofs}

If a theory has been realized, the \why printer for the corresponding prover
will no longer output declarations for that theory but instead simply put
a directive to load the realization. In order to tell the printer
that a given theory is realized, one has to add a meta declaration in the
corresponding theory section of the driver.
\begin{verbatim}
theory env_path.theory_name
  meta "realized" "env_path.theory_name", "optional_naming"
end
\end{verbatim}
The first parameter is the theory name for \why. The second
parameter, if not empty, provides a name to be used inside generated
scripts to point to the realization, in case the default name is not
suitable for the interactive prover.

\section{Generated/edited files}

\subsection{Coq}

This section describes the content of the Coq files generated by \why for
both proof obligations and theory realizations. When reading a Coq
script, \why is guided by the presence of empty lines to split the
script, so the user should refrain from removing empty lines around
generated parts or adding empty lines inside them.

\begin{enumerate}
\item	The header of the file contains all the library inclusions
	required by the driver file. Any user-made changes to this part
	will be lost when the file is regenerated by \why. This part ends
	at the first empty line.
\item	Abstract logic symbols are assumed with the vernacular directive
	\verb+Paramater+. Axioms are assumed with the \verb+Axiom+
	directive. When regenerating a script, \why assumes that all such
	symbols have been generated by a previous run. As a consequence,
	the user should not introduce new symbols with these two
	directives, as they would be lost.
\item	Definitions of functions and inductive types in theories are
	printed in a block that starts with \verb+(* Why3 assumption *)+.
	This comment should not be removed; otherwise \why will assume
	that the definition is user-made.
\item	Finally, proof obligations and symbols to be realized are
	introduced by \verb+(* Why3 goal *)+. The user is supposed to
	fill the script after the statement. \why assumes that the
	user-made part extends up to \verb+Qed+, \verb+Admitted+,
	\verb+Save+, or \verb+Defined+, whichever comes first. In the
	case of definitions, the original statement can be replaced by
	a \verb+Notation+ directive, in order to ease the usage of
	already defined symbols. \why also recognizes \verb+Variable+
	and \verb+Hypothesis+ and preserves them; they should be used in
	conjunction with Coq's \verb+Section+ mechanism to realize
	theories that still need some abstract symbols and axioms.
\end{enumerate}

Currently, the parser for Coq scripts is rather naive and does not know
much about comments. For instance, \why can easily be confused by
some terminating directive like \verb+Qed+ that would be present in a
comment.

\input{./pvs.tex}

\section{Shipping libraries of realizations}

While modifying an existing driver file might be sufficient for local
use, it does not scale well when the realizations are to be shipped to
other users. Instead, one should create two additional files: a
configuration file that indicates how to modify paths, provers, and
editors, and a driver file that contains only the needed
\verb+meta "realized"+ declarations. The configuration file should be as
follows.

\begin{verbatim}
[main]
loadpath="path/to/theories"

[prover_modifiers]
name="Coq"
option="-R path/to/vo/files Logical_directory"
driver="path/to/file/with/meta.drv"

[editor_modifiers coqide]
option="-R path/to/vo/files Logical_directory"

[editor_modifiers proofgeneral-coq]
option="--eval \"(setq coq-load-path (cons '(\\\"path/to/vo/files\\\" \
  \\\"Logical_directory\\\") coq-load-path))\""
\end{verbatim}

This configuration file can be passed to \why thanks to the
\verb+--extra-config+ option.


%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
{'fraction_non_alphanumeric': 0.06235680844705648, 'fraction_numerical': 0.0005976690905468672, 'mean_word_length': 4.4535578489951115, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5482962', 'n_tokens_mistral': 2798, 'n_tokens_neox': 2675, 'n_words': 1441}