nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues 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,607 Commits 31 Branches 0 Tags 57 MiB
Isabelle 82.2%
TeX 12.1%
Shell 3%
Scala 2.7%
Go to file
Nicolas Méric 9bc493250f Enable invariants checking everywhere 
By default invariants checking generates warnings.
if invariants_strict_checking theory option is enabled,
the checking generates errors.

Errors to resolve:
- Option type in invariant:
  See src/ontologies/scholarly_paper/scholarly_paper.thy:133

  doc_class technical = text_section +
     definition_list :: "string list" <=  "[]"
     status          :: status <= "description"
     formal_results  :: "thm list"
     invariant L1    :: "the (level σ) > 0"

  The attribute L1 uses "the" to project the level value
  but the default value is None:
  See src/ontologies/scholarly_paper/scholarly_paper.thy:69

  doc_class text_section = text_element +
   main_author :: "author option"  <=  None
   fixme_list  :: "string list"    <=  "[]"
   level       :: "int  option"    <=  "None"

  It generates an error in src/ontologies/CENELEC_50128/CENELEC_50128.thy
  for the Definition* commands, for which the level is not defined.
  It triggers an error because "the None" triggers an error.
  Get rid of the option type?

  The value None is used in the check function
  in examples/scholarly_paper/2020-iFM-CSP/paper.thy to check
  that a subsequent instance of the same class has a level >= than
  the previous instance of the same class.
  Update this function?

- What to do with the checking done in scholarly_paper (see check function)
  which use low level invariant to check the attributes?
  Migrate to High level invariant?
  If we change the default value of the level attribute in the text_lement
  class from "None" to "Some 0" then check function in scholarly_paper
  is triggered in examples/scholarly_paper/2020-iFM-CSP/paper.thy
  for the introduction instance "introtext" line 55 and generates
  a checking error.
  It comes from the fact that the previous instance introheader line 54
  is a section*, and then has a default value level of 1.
  Then, if the default value of the level attribute in the text_element
  is put to Some 0, the low level checking invariant function "check" in
  scholarly_paper triggers an error, because the "check" function
  checks that the instances in a sequence of the same class
  have a growing level.
  for a sequence: [("scholarly_paper.introduction", "introheader")
                  , ("scholarly_paper.introduction", "introtext")]
  introtext must have a level >= than introheader.
  Same issue with
  the examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
  theory.

- Bypass checking of high-level invariants
  when the class default_cid = "text",
  the top (default) document class.
  We want the class default_cid to stay abstract
  and not have the capability to be defined with attribute,
  invariants, etc.
  Hence this bypass handles docitem without a class associated,
  for example when you just want a document element to be referenceable
  without using the burden of ontology classes.
  ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close>

  The functions get_doc_class_global and get_doc_class_local trigger
  an error when the class is "text" (default_cid),
  then the functions like check_invariants which use it will fail
  if the checking is enabled by default for all the theories.

A quick and dirty fix is proposed to pass the compilation, but must be revised.
See the diff.
 		2022-12-14 18:23:18 +01:00
.woodpecker Tuned messages and options, following Isabelle/c7f3e94fce7b 2022-12-05 12:37:59 +01:00
etc More formal management of ontologies in Isabelle/ML/Isar with output via Isabelle/Scala exports 2022-12-04 00:09:29 +01:00
examples Enable invariants checking everywhere 2022-12-14 18:23:18 +01:00
src Enable invariants checking everywhere 2022-12-14 18:23:18 +01:00
.gitattributes Initial commit. 2022-07-07 22:43:25 +01:00
.gitignore Ignore Isabelle/JEdit tmp files. 2022-03-26 19:56:23 +00:00
CHANGELOG.md Update to Isabelle 2022. 2022-10-30 17:56:15 +00:00
CITATION Fixed file attributes. 2022-04-18 09:44:44 +01:00
LICENSE Fixed file attributes. 2022-04-18 09:44:44 +01:00
README.md Tuned messages and options, following Isabelle/c7f3e94fce7b 2022-12-05 12:37:59 +01:00
ROOTS Fixed file attributes. 2022-04-18 09:44:44 +01:00
install-afp Prefer DOF parameters over Isabelle options 2022-12-03 12:37:58 +01: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 and formal development. The manual for Isabelle/DOF 1.3.0/Isabelle2021-1 is available online.

Pre-requisites

Isabelle/DOF has three major prerequisites:

Installation

Isabelle/DOF is provided as an Isabelle component. After installing the prerequisites, change into the directory containing Isabelle/DOF (this should be the directory containing this README.md file) and execute (if you executed this command already during the installation of the prerequisites, you can skip it now):

foo@bar:~$ isabelle components -u .

The 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 dof_mkroot

The dof_mkroot 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 dof_mkroot -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 dof_mkroot -h

Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY]

  Options are:
    -I           init Mercurial repository and add generated files
    -h           print help
    -n NAME      alternative session name (default: directory base name)
    -o NAMES     list of ontologies, separated by blanks
                 (default: "technical_report scholarly_paper")
    -q           quiet mode: less verbosity
    -t NAME      template (default: "scrreprt-modern")

  Create session root directory for Isabelle/DOF (default: current directory).

Releases

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

Older Releases

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

Upstream Repository

The upstream git repository, i.e., the single source of truth, for this project is hosted at https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF.