From 403bffff83ab67311d4eec879f3a8efdc6acc87a Mon Sep 17 00:00:00 2001 From: Sankalp Gambhir Date: Mon, 13 Nov 2023 15:25:29 +0100 Subject: [PATCH] Update README --- README.md | 108 ++++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 81 insertions(+), 27 deletions(-) diff --git a/README.md b/README.md index 17bc6e24..de6a6081 100644 --- a/README.md +++ b/README.md @@ -1,47 +1,101 @@ # LISA = LISA Is Sets Automated -LISA is a Proof Assistant based on first order logic, sequent calculus and set theory. To get started, look at the [Reference Manual](Reference%20Manual/lisa.pdf). +LISA is a proof assistant based on first-order logic, sequent calculus, and set +theory. To get started, take a look at the [Reference +Manual](Reference%20Manual/lisa.pdf). -EPFL-LARA Website: https://lara.epfl.ch/w/ +LISA is developed and maintained by the [Laboratory for Automated Reasoning and +Analysis (LARA)](https://lara.epfl.ch) at the [EPFL](https://epfl.ch). + +For details regarding the design of LISA and techniques implemented here, you +can check the following publications: + + - Guilloud, S., Bucev, M., Milovančević, D., Kunčak, V. (2023). Formula + Normalizations in Verification. In: Enea, C., Lal, A. (eds) Computer Aided + Verification. CAV 2023. Lecture Notes in Computer Science, vol 13966. + Springer, Cham. https://doi.org/10.1007/978-3-031-37709-9_19 + - Simon Guilloud, Sankalp Gambhir, and Viktor Kunčak. LISA - A Modern Proof + System. In 14th International Conference on Interactive Theorem Proving (ITP + 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, + pp. 17:1-17:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023) + https://doi.org/10.4230/LIPIcs.ITP.2023.17 ## Installation and utilisation - - You first need to [install Scala on your system](https://www.scala-lang.org/download/). - - Then, clone the presen project. - - In the root folder, type `sbt`. - - To execute a file in LISA's Mathematical Library, type `run` and select a file (try with `SetTheory.scala` first!). SBT will install missing packages and compile the project, and output the theorems of the file. - - To experiment with the system, type `project lisa-examples`. - - We recommand using VSCode or Intelliji to edit lisa code. Create a new file in the lisa-examples folder. You can use the file `Examples.scala` as a template. + + - First, [install Scala 3 on your system per the official + instructions](https://www.scala-lang.org/download/). You should have obtained + Scala 3 and [SBT](https://www.scala-sbt.org/). + - Then, clone the present project. + - In the root folder, run `sbt`. + - To execute a file in LISA's Mathematical Library, type `run` in the `sbt` + interactive console and select a main class to run when prompted (try with + `SetTheory.scala` first!). + - On the first run, SBT will install missing packages and compile the project, + and outputting the theorems proved in the chosen file. + - To experiment with the system, type `project lisa-examples`, and play around + with the examples in + [lisa-examples/src/main/scala/Example.scala](lisa-examples/src/main/scala/Example.scala), + or create your own file. You can start your own LISA file with the following + minimal header: + ```scala + object MyLisaFile extends lisa.Main { + // your proofs go here + } + ``` + - We recommend using [Visual Studio Code](https://code.visualstudio.com/) with + the [Metals extension](https://scalameta.org/metals/) or [JetBrains IntelliJ + IDEA](https://www.jetbrains.com/idea/) to edit LISA code. ## Project Organisation ### Kernel -The kernel package contains the trusted code of LISA, in the sense that it only can produce theorem and verify proof. Any bug or error in code written outside this package should not possibly break soundness. -The kernel contains essentially two elements: Formalisation of First Order Logic, and Formalisation of Proofs through Sequent Calculus. + +The `lisa-kernel` package contains the trusted code of LISA, in the sense that +all theorems and proofs pass through it to be considered correct. It only can +produce theorems and verify proof. Any bug or error in code written outside this +package should not possibly break soundness. + +The kernel essentially contains two elements: formalisation of first-order +logic, and formalisation of proofs through sequent calculus. ### Utils -The utils package contains a set of utilities to interract with the kernel. Syntactic sugar, a parser and printer for proofs and formulas, interraction with tptp library, unification algorithms. The package also contains LISA's DSL to write proofs, tactics and mathematical developments. -## Commands +The `lisa-utils` package contains a set of utilities to interact with the +kernel. Syntactic sugar, a parser and printer for proofs and formulas, +unification algorithms, among others. The package also contains LISA's DSL to +write proofs, tactics, and mathematical developments. + +Most user-developed tactics, syntax, and auxiliary utilities go here. + +## Interacting with the project + +The following commands can be used to perform different actions as configured in +the project. Each command ("`command`") can be run within the `sbt` console as +simply `command` or in batch mode from a shell session in the project directory +with `sbt command` or `sbt "command; command; ..."`. + +* `run` to execute a LISA file, prompting which file to run +* `runMain classPath` to run a specific main file at `classPath` without prompt. + * For example: `runMain lisa.mathematics.settheory.SetTheory` +* `test` to compile and execute the test suite +* `assembly` to package LISA as a library +* `doc` to generate the Scala documentation +* `scalafix` to lint the whole project +* `scalafmt` to format the whole project -* `sbt test` to compile and execute the test suite -* `sbt assembly` to package it as a library -* `sbt doc` to generate the Scala documentation -* `sbt run` to execute a LISA file -* `sbt scalafix` to lint the whole codebase -* `sbt scalafmt` to format the whole codebase +## License and Distribution -## LICENSE - Copyright 2023 EPFL + Copyright © 2023 EPFL - Licensed under the Apache License, Version 2.0 (the "License"); - you may not use this file except in compliance with the License. - You may obtain a copy of the License at + Licensed under the Apache License, Version 2.0 (the "License"); you may not + use this file except in compliance with the License. You may obtain a copy of + the License at http://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software - distributed under the License is distributed on an "AS IS" BASIS, - WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - See the License for the specific language governing permissions and - limitations under the License. + distributed under the License is distributed on an "AS IS" BASIS, WITHOUT + WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the + License for the specific language governing permissions and limitations under + the License.