Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity
Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting as well as formal development.
1,225 Commits 14 Branches 9 Tags 76 MiB
Isabelle 56.4%
TeX 41.9%
Scala 0.9%
Shell 0.8%
Go to file
Nicolas Méric 2c01a7118b Add term* cmd and term antiquotations for classes 
- Add a term antiquotation for document classes
  and add the term* command which mimics the classical term command
  and adds the possibility to use a term antiquotation
  which references document classes:
  one can use @{A ''A_instance''} to reference
  an instance of the class A in a term* command.
- Reuse and update the ML_isa_check_generic visitor pattern
  to add the function which checks the class instance of a class,
  used by the term antiquotation for document classes.
  Also, the update_isa functions now expect long name
  (See builtin term antiquotations setup)
- The merge of ISA_transformer_tab has been update to avoid conflicts.
  Indeed, the merge is ultra-critical: the transformer tabs were
  just extended by letting *the first* entry
  with the same long-name win.
  Since the range is a (call-back) function, a comparison on its content
  is impossible and some choice has to be made.
  An alternative may be to use Symtab.join
- As classes names as constants are already bound to
  "doc_class Regular_Exp.rexp" constants by add_doc_class_cmd function,
  we use a prefix "doc_class_" when adding
  document classes term antiquotations
 		2021-06-01 17:32:45 +02:00
.ci Updated Isabelle base image. 2021-03-21 00:00:13 +00:00
examples all changes 2021-06-01 14:51:22 +02:00
src Add term* cmd and term antiquotations for classes 2021-06-01 17:32:45 +02:00
.config Update after Isabelle/DOF 1.1.0/Isabelle2021 release. 2021-03-20 23:56:46 +00:00
.gitattributes mmm 2020-06-22 17:42:40 +02:00
.gitignore mmm 2020-06-22 17:42:40 +02:00
CHANGELOG.md Added v.1.1.0. 2021-03-20 22:25:29 +00:00
CITATION mmm 2020-06-22 17:42:40 +02:00
LICENSE mmm 2020-06-22 17:42:40 +02:00
README.md Updated TeX Live dependency to version 2021. 2021-04-01 23:47:35 +01:00
ROOTS mmm 2020-06-22 17:42:40 +02:00
install Removed check for \expanded{}: Isabelle 2021 defaults to luatex as TeX-engine, which has \expanded{} since a very long time. 2021-03-10 22:10:12 +00:00

README.md

Isabelle/DOF: Document Preparation Setup

Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting as well as formal development. The manual for Isabelle/DOF 1.1.0/Isabelle2021 is available online.

Running Isabelle/DOF using Docker

As an alternative to installing Isabelle/DOF locally, the latest official release Isabelle/DOF is also available on Docker Hub. Thus, if you have Docker installed and your installation of Docker supports X11 application, you can start Isabelle/DOF as follows:

foo@bar:~$ docker run -ti --rm -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix \ 
           logicalhacking/isabelle_dof-1.1.0_isabelle2021 isabelle jedit

Pre-requisites

Isabelle/DOF has two major pre-requisites:

  • Isabelle: Isabelle/DOF requires Isabelle 2021. Please download the Isabelle 2021 distribution for your operating system from the Isabelle website.
  • LaTeX: Isabelle/DOF requires a modern LaTeX installation, i.e., at least TeX Live 2021 with all available updates applied.

Installation

In most case, the DOF-plugin can be installed as follows:

foo@bar:~$ ./install

If a specific Isabelle version should be used (i.e., not the default one), the full path to the isabelle command needs to be passed as using the --isabelle command line argument of the install script:

foo@bar:~$ ./install --isabelle /usr/local/Isabelle2021/bin/isabelle

For further command line options of the installer, please use the built-in help:

foo@bar:~$ ./install --help

A final step for the installation is:

foo@bar:~$ isabelle build -D .

This will compile Isabelle/DOF and run the example suite.

Usage

Opening an Example

If you want to work with or extend one of the examples, e.g., you can open it similar to any standard Isabelle theory:

isabelle jedit -d . -l Isabelle_DOF examples/scholarly_paper/2018_cicm/IsaDofApplications.thy

This will open an example of a scientific paper using the pre-compiled session Isabelle_DOF, i.e., you will not be able to edit the ontology definitions. If you want to edit the ontology definition, just open the theory file with the default HOL session:

isabelle jedit -d . -l HOL examples/scholarly_paper/2018_cicm/IsaDofApplications.thy

While this gives you more flexibility, it might "clutter" your editing experience, as a lot of internal theories are loaded into Isabelle's editor.

Creating a New Project

The DOF-plugin provides an alternative to Isabelle's mkroot command. Isabelle projects that use DOF need to be created using

foo@bar:~$ isabelle mkroot_DOF

The mkroot_DOF command takes the same parameter as the standard mkroot command of Isabelle. Thereafter, the normal Isabelle command for building documents can be used.

Using the -o option, different ontology setups can be selected and using the -t option, different LaTeX setups can be selected. For example,

foo@bar:~$ isabelle mkroot_DOF -o scholarly_paper -t scrartcl

creates a setup using the scholarly_paper ontology and the article class from the KOMA-Script bundle.

The help (option -h) show a list of all supported ontologies and document templates:

foo@bar:~$ isabelle mkroot_DOF -h

Usage: isabelle mkroot_DOF [OPTIONS] [DIR]

  Options are:
    -h           print this help text and exit
    -n NAME      alternative session name (default: DIR base name)
    -o ONTOLOGY  (default: scholarly_paper)
       Available ontologies:
       * cenelec_50128
       * mathex
       * scholarly_paper
    -t TEMPLATE   (default: scrartcl)
       Available document templates:
       * lncs
       * scrartcl
       * scrreprt
       * scrreprt-modern

  Prepare session root DIR (default: current directory).

Releases

For releases, signed archives including a PDF version of the Isabelle/DOF manual are are available:

Team

Main contacts:

Contributors

  • Idir Ait-Sadoune
  • Paolo Crisafulli
  • Chantal Keller
  • Nicolas Méric

License

This project is licensed under a 2-clause BSD license.

SPDX-License-Identifier: BSD-2-Clause

Publications

Master Repository

The master git repository for this project is hosted https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF.