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.
2,022 Commits 31 Branches 0 Tags 57 MiB
Isabelle 82.2%
TeX 12.1%
Shell 3%
Scala 2.7%
Go to file
Nicolas Méric a31098c98d Ongoing handling of ide interaction for string attributes 
Ongoing handling of ide interaction
of string type attribute value of instances as input source.

The idea is when an attribute is a string type, then
handle its value as an input source so that
interaction with PIDE will be optimal:
- if the attribute is not a string type then we parse it using
  Parse.term
- if this is a string type, then we parse it with Parse.document_source
  and then we convert it to a string
  and try to parse it as a term.
  If the parsing fails,
  we handle the error and update the string by enclosing it with
  cartouches so that it can be understand as a hol string using
  frederic tuong hol string implementation
  (hol string declared with cartouche and not double simple quotes).
  Then we pass it to
  the code that generate the instance (cmd function).
  If this is not a
  well formed hol string we get an error.
 		2023-12-21 12:29:18 +01:00
.woodpecker Test with Isabelle 2023. 2023-09-14 06:29:01 +01:00
Isabelle_DOF Ongoing handling of ide interaction for string attributes 2023-12-21 12:29:18 +01:00
Isabelle_DOF-Example-I Use binding for instances name 2023-07-20 10:11:48 +02:00
Isabelle_DOF-Example-II Polymorphic classes first draft 2023-07-19 18:58:04 +02:00
Isabelle_DOF-Examples-Extra Ongoing handling of ide interaction for string attributes 2023-12-21 12:29:18 +01:00
Isabelle_DOF-Ontologies Moved default value for title into template, as some LaTeX classes do not allow for a pre-set title. 2023-08-04 04:37:14 +01:00
Isabelle_DOF-Proofs Update instances list term antiquotation 2023-09-11 09:07:10 +02:00
Isabelle_DOF-Unit-Tests Ongoing handling of ide interaction for string attributes 2023-12-21 12:29:18 +01:00
etc Build document build engine also for main Isabelle/DOF component. 2023-03-13 13:00:49 +00:00
scala Initial implementation of list_templates and list_ontologies (fixes #28). 2023-02-27 08:39:53 +00:00
.gitattributes Initial commit. 2022-07-07 22:43:25 +01:00
.gitignore Ignore generated latex-outputs in test session. 2023-02-25 11:01:58 +00:00
CHANGELOG.md Documented Isabelle version (2023). 2023-09-14 06:33:28 +01: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 Documented Isabelle version (2023). 2023-09-14 06:33:28 +01:00
README_DEVELOPMENT.md Test with Isabelle 2023. 2023-09-14 06:29:01 +01:00
ROOTS Fixed archive building after session renaming. 2023-04-15 16:52:25 +01:00
install-afp Added new dependency: Metalogic_ProofChecker 2023-03-01 10:19:29 +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 and formal development.

Pre-requisites

Isabelle/DOF has two major prerequisites:

Installation

Installation of the Development Version (Git Repository)

The development version of Isabelle/DOF that is available in this Git repository provides, over the AFP version, additional ontologies, document templates, and examples that might not yet "ready for general use". Furthermore, as it is provided as an Isabelle component, it can also provide additional tools that cannot be distributed via the AFP. For more details on installing the development version, please consult the README_DEVELOPMENT.md file.

After installing the prerequisites, change into the directory containing Isabelle/DOF (this should be the directory containing this README.md file) and execute the following command for building the standard sessions of Isabelle/DOF:

foo@bar:~$ isabelle build -D . -x Isabelle_DOF-Proofs -x HOL-Proofs

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

For building the session Isabelle_DOF-Proofs, the timeout might need to increased to avoid timeouts during building the dependencies:

foo@bar:~$ isabelle build -d . -o 'timeout_scale=2' Isabelle_DOF-Proofs

Usage

In the following, we assume that you installed Isabelle/DOF either from the AFP (adding the AFP as a component to your Isabelle system) or from the Git repository of Isabelle/DOF (installing Isabelle/DOF as a component to your Isabelle system).

Assuming that your current directory contains the example academic paper in the subdirectory Isabelle_DOF-Example-I/, you can open it similar to any standard Isabelle theory:

isabelle jedit -l Isabelle_DOF Isabelle_DOF-Example-I/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 default ontologies defined in the Isabelle_DOF session. If you want to edit the ontology definition, just open the theory file with the session Functional-Automata:

isabelle jedit -l Functional-Automata Isabelle_DOF-Example-I/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.

Repository Structure

The main branch of this Repository is developed using the latest official release of Isabelle. This is also the main development branch. In addition, he Isabelle_dev branch is used for testing Isabelle/DOF with the latest development version of Isabelle.

This repository is structured into several Isabelle sessions, each of which is stored in a subdirectory:

  • Isabelle_DOF: This is the main session, providing the Isabelle/DOF system. Furthermore, this session is currently under consideration for a submission to the AFP.
  • Isabelle_DOF-Example-I: This session provides an example document written Isabelle/DOF. It only requires the core ontologies provided by the Isabelle_DOF session. Furthermore, this session is currently under consideration for a submission to the AFP.
  • Isabelle_DOF-Ontologies: This session provided additional ontologies and document templates.
  • Isabelle_DOF-Unit-Tests: This session includes various tests for the Isabelle/DOF system, partly depending on the ontologies provided by the Isabelle_DOF-Ontologies session.
  • Isabelle_DOF-Examples-Extra: This directory contains additional example documents written using the Isabelle/DOF systems, each of which is defined in an own subdirectory.
  • Isabelle_DOF-Proofs: This session provides the Isabelle/DOF systems with proof objects. This is required for the deep ontology embedding.

Releases

For releases, signed archives including a PDF version of the Isabelle/DOF manual are available. The latest release is Isabelle/DOF 1.3.0/Isabelle2021-1:

Older releases are available here.

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.