Experimental mirror of Citadelle ( https://projects.brucker.ch/hol-testgen/log/trunk/hol-testgen/add-ons/Featherweight-OCL ) compiling with randomly selected versions of Isabelle
You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
91 lines
3.1 KiB
91 lines
3.1 KiB
This directory contains the detailed AFP submission of the
|
|
"Featherweight OCL" semantics for OCL as well as our proposal
|
|
for Appendix A of the OCL standard.
|
|
|
|
Beyond the standard mechanism
|
|
|
|
(* < *)
|
|
<<skipped isar text, not shown in doc >>
|
|
(* > *)
|
|
|
|
The two main targets of this Isabelle project are:
|
|
- check everything and generate all documents allowing "sorry"'s, i.e.,
|
|
using Isabelles "quick-and-dirty"-mode:
|
|
|
|
isabelle build -c -d . -v -b OCL-dirty
|
|
|
|
- check everything and generate all documents, ensuring that
|
|
no "sorry"'s are used:
|
|
|
|
isabelle build -c -d . -v -b OCL
|
|
|
|
In your LaTeX text, you can use the following two PlainTeX
|
|
environments for selecting in which version your text should
|
|
appear:
|
|
|
|
\isatagafp
|
|
This text will only be visible in the AFP submission, i.e.,
|
|
document.pdf and outline.pdf.
|
|
\endisatagafp
|
|
|
|
\isatagannexa
|
|
This text will only be visible in the Annex A, i.e., annex-a.pdf.
|
|
\endisatagannexa
|
|
|
|
|
|
Note that these tags only work within regular Isabelle/Isar "text"
|
|
commands if they are complete, i.e.:
|
|
|
|
text {* ... \isatagafp ... \endisatagafp ...*}
|
|
|
|
Only opening or closing such a tag in Isabelle/Isar "text" commands
|
|
will not work. For this, you need to use the "text_raw" command:
|
|
|
|
text_raw {* \isatagafp *}
|
|
...
|
|
text_raw {* \endisatagafp *}
|
|
|
|
|
|
For working, these tags rely on the file comment.sty, which
|
|
is automatically added by Isabelle during the document generation.
|
|
However at the time of writing, the current comment.sty included by
|
|
Isabelle (version 3.6) mentions:
|
|
"The opening and closing commands should appear on a line
|
|
of their own. No starting spaces, nothing after it."
|
|
In particular, it is not advised to put these tags in a single line:
|
|
\isatagafp ... \endisatagafp % wrong
|
|
otherwise as side effects some parts occurring after these tags may be
|
|
skipped. The recommanded solution is to always write each tag in a
|
|
separate line:
|
|
\isatagafp
|
|
...
|
|
\endisatagafp
|
|
|
|
|
|
Warning:
|
|
=======
|
|
Please check twice that you are using \isatagX and \endisatagX
|
|
properly, i.e.,
|
|
- always pairwise matching
|
|
- not separating other envirments.
|
|
Not using these PlainTeX environments (which are, generally,
|
|
obsolete and discouraged but used by the Isabelle LaTeX setup
|
|
anyhow. We only use them to avoid introducing a parallel setup to
|
|
the one that we cannot avoid due to design decisions by the
|
|
Isabelle maintainer) carefully, will result in LaTeX errors that
|
|
are close to not debug-able.
|
|
|
|
|
|
List of Isabelle versions to use depending on revisions:
|
|
=========================================================
|
|
2018/02/05 revision 13265: Isabelle2017 (October 2017)
|
|
2018/01/29 revision 13259: Isabelle2016-1 (December 2016)
|
|
2016/02/22 revision 12439: Isabelle2016 (February 2016)
|
|
2015/06/11 revision 11691: Isabelle2015 (May 2015)
|
|
2015/02/02 revision 11283: Isabelle2014 (August 2014)
|
|
2013/12/05 revision 10054: Isabelle2013-2 (December 2013)
|
|
2013/12/02 revision 10013: Isabelle2013-1 (November 2013)
|
|
2013/11/14 revision 9950: Isabelle2013 (February 2013)
|
|
2013/05/27 revision 9682: Isabelle2012 (May 2012)
|
|
(* 2013/03/27 revision 9616 *)
|
|
revision ?: Isabelle2011-1 (October 2011)
|
|
|