Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
This commit is contained in:
commit
618997f34c
|
|
@ -0,0 +1,107 @@
|
|||
(*<*)
|
||||
theory "05_IsaDofLaTeX"
|
||||
imports "04_RefMan"
|
||||
begin
|
||||
(*>*)
|
||||
|
||||
chapter*[latex::technical,main_author="Some(@{docitem ''adb''}::author)"]\<open> PDF Generation with \isadof \<close>
|
||||
|
||||
|
||||
section*[latex1::technical]\<open>How to adapt \isadof to a new document style file\<close>
|
||||
|
||||
text\<open>Current \isadof comes with a number of setups for the PDF generation, notably
|
||||
Springer LNCS, lipics, ..., as well as setupqs of technical reports this the present one.
|
||||
|
||||
The question arises, what to do if \isadof has to be accoustomed to a new LaTeX style
|
||||
file configuration in order to generate PDF.
|
||||
\<close>
|
||||
text\<open>
|
||||
In theory, this is simple - in practice, the efforts required
|
||||
depends mostly on two factors:
|
||||
|
||||
\<^item> how compatible is the required LaTeX class with Isabelle's LateX
|
||||
setup in general (e.g., does it work with an antique version
|
||||
of \<open>comment.sty\<close> required by Isabelle)
|
||||
|
||||
\<^item> how much magic does the required LaTeX class wrt the title page
|
||||
information (author, affiliation).
|
||||
|
||||
\<^item> which ontologies should be supported. While most ontologies are
|
||||
generic, some only support a very specific subset of LaTeX
|
||||
templates (classes). For example, \<^theory_text>\<open>scholarly_paper\<close> does currently
|
||||
\<^emph>\<open>only\<close> support \<open>llncs\<close>, \<open>rartcl\<close>, and \<open>lipics\<close>.
|
||||
|
||||
The general process as such is straight-forward:
|
||||
|
||||
\<^enum> From the supported LaTeX classes, try to find the one that is
|
||||
most similar to the one that you want to support. For the sake
|
||||
of the this example, let's assume this is llncs
|
||||
\<^enum> Use the template for this class (llncs) as starting point, i.e.,
|
||||
\<^verbatim>\<open>cp document-generator/document-template/root-lncs.tex
|
||||
document-generator/document-template/root-eptcs.tex\<close>
|
||||
|
||||
The mandatory naming scheme for the templates is
|
||||
|
||||
\<^verbatim>\<open>root-<TEMPLATE_NAME>.tex\<close>
|
||||
|
||||
That is to say that \<^verbatim>\<open><TEMPLATE_NAME>\<close> should be the name of the
|
||||
new LaTeX class (all lowercase preferred) that will be used
|
||||
in config files and also will be shown in the help text
|
||||
shown by executing
|
||||
|
||||
\<^verbatim>\<open>isabelle DOF_mkroot -h\<close>
|
||||
|
||||
\<^enum> Edit the new template as necessary (using the provided
|
||||
example from the target class as reference):
|
||||
|
||||
\<^verbatim>\<open>vim document-generator/document-template/root-foo.tex\<close>
|
||||
|
||||
and do the needful.
|
||||
|
||||
\<^enum> Install the new template:
|
||||
|
||||
\<^verbatim>\<open>./install\<close>
|
||||
|
||||
(If you have a working installation of the required AFP entries
|
||||
and the Isabelle/DOF patch, you can use \<^verbatim>\<open>./install -s\<close>
|
||||
which will \<^emph>\<open>ONLY\<close> install the \<^verbatim>\<open>LaTeX styles/templates\<close>, see
|
||||
\<^verbatim>\<open>./install -h)\<close>
|
||||
|
||||
\<^enum> Now the new template should be available, you can check this with
|
||||
|
||||
\<^verbatim>\<open>isabelle DOF_mkroot -h\<close>
|
||||
|
||||
\<^enum> Create an "tiny/empty" Isabelle project using the ontology "core"
|
||||
and test your template. If everything works, celebrate. If it does
|
||||
not work, understand what you need to change and continue
|
||||
with step 3.
|
||||
|
||||
(of course, if the new class is not available in TeXLive, you need
|
||||
to add them locally to the documents folder of your Isabelle
|
||||
project and, as usual, it needs to be registered in your ROOTS
|
||||
file)
|
||||
|
||||
\<^enum> If the ontologies that should be used together with this LaTeX
|
||||
class do not require specific adaptions (e.g., CENELEC 50128),
|
||||
everything should work. If one of the required ontology LaTeX
|
||||
setups only supports a subset of LaTeX classes (e.g., \<^theory_text>\<open>scholarly_paper\<close>
|
||||
due to the different setups for authors/affiliations blurb),
|
||||
you need to develop support for you new class in the ontology
|
||||
specific LaTeX styles, e.g.,
|
||||
\<open>document-generator/latex/DOF-scholarly_paper.sty\<close>
|
||||
(mandatory naming convention: \<open>DOF-<ONTOLOGY_NAME>.sty\<close>)
|
||||
|
||||
\<^enum> After updating the ontology style (or styles), you need
|
||||
to install them (again, you might want to use ./install -s)
|
||||
and test your setup with a paper configuration using
|
||||
your new LaTeX template and the required styles. In case
|
||||
of errors, go back to step 7.
|
||||
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
(*<*)
|
||||
end
|
||||
(*>*)
|
||||
|
||||
|
|
@ -0,0 +1,70 @@
|
|||
(*<*)
|
||||
theory "06_Conclusion"
|
||||
imports "05_IsaDofLaTeX"
|
||||
begin
|
||||
(*>*)
|
||||
|
||||
chapter*[conclusion::conclusion]\<open> Conclusion and Related Work\<close>
|
||||
text\<open> We have demonstrated the use of \isadof, a novel ontology modeling and enforcement
|
||||
IDE deeply integrated into the Isabelle/Isar Framework. The two most distinguishing features are
|
||||
\<^item> \isadof and its ontology language are a strongly typed language that allows
|
||||
for referring (albeit not reasoning) to entities of Isabelle/HOL, most notably types, terms,
|
||||
and (formally proven) theorems, and
|
||||
\<^item> \isadof is supported by the Isabelle/PIDE framework; thus, the advantages of an IDE for
|
||||
text-exploration (which is the type of this link? To which text element does this link refer?
|
||||
Which are the syntactic alternatives here?) were available during editing
|
||||
instead of a post-hoc validation process.\<close>
|
||||
|
||||
text\<open> Of course, a conventional batch-process also exists which can be used
|
||||
for the validation of large document bases in a conventional continuous build process.
|
||||
This combination of formal and semi-informal elements, as well as a systematic enforcement
|
||||
of the coherence to a document ontology of the latter, is, as we believe, novel and offers
|
||||
a unique potential for the semantic treatment of scientific texts and technical documentations. \<close>
|
||||
|
||||
text\<open> To our knowledge, this is the first ontology-driven framework for editing mathematical and
|
||||
technical documents that focuses particularly on documents mixing formal and informal content---a
|
||||
type of documents that is very common in technical certification processes. We see mainly one
|
||||
area of related works: IDEs and text editors that support editing and checking of documents based
|
||||
on an ontology. There is a large group of ontology editors (\eg, Prot{\'e}g{\'e}~@{cite "protege"},
|
||||
Fluent Editor~@{cite "cognitum"}, NeOn~@{cite "neon"}, or OWLGrEd~@{cite "owlgred"}). With them,
|
||||
we share the support for defining ontologies as well as auto-completion when editing documents
|
||||
based on an ontology. While our ontology definitions are currently based on a textual definition,
|
||||
widely used ontology editors (\eg, OWLGrEd~@{cite "owlgred"}) also support graphical notations.
|
||||
This could be added to \isadof in the future. A unique feature of \isadof is the deep integration
|
||||
of formal and informal text parts. The only other work in this area we are aware of is
|
||||
rOntorium~@{cite "rontorium"}, a plugin for Prot{\'e}g{\'e} that integrates
|
||||
R~@{cite "adler:r:2010"} into an ontology environment. Here, the main motivation behind this
|
||||
integration is to allow for statistically analyze ontological documents. Thus, this is
|
||||
complementary to our work. \<close>
|
||||
|
||||
text\<open> \isadof in its present form has a number of technical short-comings as well
|
||||
as potentials not yet explored. On the long list of the short-comings is the
|
||||
fact that tables are at present not supported, and a test-execution environment
|
||||
for external test-executions is missing. For the moment, \isadof is conceived as an
|
||||
add-on for Isabelle/HOL; a much deeper integration of \isadof into Isabelle
|
||||
could increase both performance and uniformity. Finally, different target
|
||||
presentation (such as HTML) would be highly desirable in particular for the
|
||||
math exam scenarios. And last but not least, it would be desirable that PIDE
|
||||
itself is ``ontology-aware'' and can, for example, use meta-information
|
||||
to control read- and write accesses of \<^emph>\<open>parts\<close> of documents. An important
|
||||
other direction to explore is \<^emph>\<open>out-of-order\<close> presentation, \ie{} a systematic
|
||||
approach to present a document in another than the usual linear \<^emph>\<open>definition-before-use\<close>
|
||||
order.\<close>
|
||||
|
||||
|
||||
|
||||
subsubsection\<open>Availability.\<close>
|
||||
text\<open> The implementation of the framework is available at
|
||||
@{url \<open>https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/\<close>}.
|
||||
\isadof is licensed under a 2-clause BSD license (SPDX-License-Identifier: BSD-2-Clause).\<close>
|
||||
|
||||
|
||||
subsubsection\<open>Acknowledgments.\<close>
|
||||
text\<open>This work has been partially supported by IRT SystemX, Paris-Saclay, France, and
|
||||
therefore granted with public funds of the Program ``Investissements d'Avenir.''\<close>
|
||||
|
||||
|
||||
(*<*)
|
||||
end
|
||||
(*>*)
|
||||
|
||||
Loading…
Reference in New Issue