Data

Tools

Indexes

Applications

Experiments

Open Source Science

master-project

Master Thesis Project at LARA (EPFL)

https://github.com/floriancassayre/master-project

Science Score: 67.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ✓
    CITATION.cff file
    Found CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ✓
    .zenodo.json file
    Found .zenodo.json file
  • ✓
    DOI references
    Found 3 DOI reference(s) in README
  • ✓
    Academic publication links
    Links to: zenodo.org
  • ○
    Committers with academic emails
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (12.3%) to scientific vocabulary

Keywords

epfl formal-methods lisa proof-assistant proof-system sequent-calculus set-theory
Last synced: 6 months ago · JSON representation ·

Repository

Master Thesis Project at LARA (EPFL)

Basic Info
  • Host: GitHub
  • Owner: FlorianCassayre
  • License: mit
  • Language: Scala
  • Default Branch: master
  • Homepage:
  • Size: 940 KB
Statistics
  • Stars: 3
  • Watchers: 2
  • Forks: 0
  • Open Issues: 0
  • Releases: 3
Topics
epfl formal-methods lisa proof-assistant proof-system sequent-calculus set-theory
Created about 4 years ago · Last pushed over 3 years ago
Metadata Files
Readme License Citation

README.md

Florian Cassayre's Master Project

CI Version Last commit License DOI

This repository hosts the work related to my Master Project (PDM) at LARA. This includes source code, writeup and any other significant resource related to the project.

Project title: A front-end for the LISA proof assistant

Dates: 21.02.2022 to 24.06.2022

Content: In this project I will be working on a proof assistant (LISA), in particular I will be designing a higher-level interface to represent and write proofs.

Installation as a library

The repository can be used as a sbt dependency. Since LISA is not yet published, you are responsible for including LISA in your project as a dependency.

Details on how to do so are described below.

Installing LISA There are two main possibilities for installing LISA. In either case, it's very important that the version of LISA matches the one used by this project, otherwise you might encounter incompatibilities. Assuming you are in your project's directory and `$COMMIT` is the hash of the desired commit in LISA: * **sbt managed dependency** (easiest): * Add the following in your `build.sbt` (or adapt your existing configuration): ```sbt lazy val lisa = ProjectRef(uri("https://github.com/epfl-lara/lisa.git#$COMMIT"), "lisa") lazy val root = (project in file(".")).dependsOn(lisa) ``` * **git repository or submodule** (if you need to develop on LISA at the same time): * If your project **is already** a git repository, then you can add LISA as a submodule: ``` git submodule add git@github.com:epfl-lara/lisa.git lisa cd lisa git checkout $COMMIT cd .. git commit ``` * If your project **is not** a git repository, then you can clone it locally: ``` git clone git@github.com:epfl-lara/lisa.git cd lisa git checkout $COMMIT cd .. ``` The table below indicates the version compatibility (= value of `$COMMIT`): | `master-project` | `lisa` | |:----------------:|:------------------------------------------:| | `1.0.0` | `3ae1c204df54e780ab7565070575b421b119f684` | | `0.2.0` | `eacb9c06aa2975b9ae2bc993847c597eb3c54995` | | `0.1.0` | `eacb9c06aa2975b9ae2bc993847c597eb3c54995` |

Then, add these two lines to your build.sbt: ```sbt resolvers += "Florian Cassayre" at "https://maven.cassayre.me"

libraryDependencies += "me.cassayre.florian" %% "master-project" % "0.2.0" ```

Or alternatively, if you would like to include it from the sources:

```sbt lazy val lisa = ??? lazy val masterproject = ProjectRef(uri("https://github.com/FlorianCassayre/master-project.git#$COMMIT"), "lisa")

lazy val root = (project in file(".")).dependsOn(lisa, masterproject) ```

(replace $COMMIT by the commit hash)

Structure

  • Source code
    • front: the implementation of the front
    • util: some utilities for LISA
    • legacy: old proof-of-concept implementations that are kept for reference
    • test: main methods that serve as examples or test files
  • Weekly notes relating the work done stating the future objectives
  • Documentation about the various components
  • Thesis the deliverables other than the code itself

Development

Clone the repository: git clone git@github.com:FlorianCassayre/master-project.git --recurse-submodules --remote-submodule

(or run git submodule update --init --recursive if you have already cloned the repository without initializing the submodules).

The relevant commands are:

  • sbt console to start a REPL session
  • sbt test to run the tests
  • sbt publish to generate the artifacts under releases/
Updating LISA The git submodule depends on a specific commit, thus when LISA is updated _and_ we would like to benefit from the changes, we should execute the following commands: ```bash cd lisa git pull origin main cd .. git add lisa git commit lisa ``` (make sure to rebuild the entire project after this operation, to avoid potential issues with incremental compilation)

Licensing

This project is licensed under the MIT License.

LISA is licensed under the Apache License 2.0.

Owner

  • Name: Florian Cassayre
  • Login: FlorianCassayre
  • Kind: user
  • Location: France · Switzerland
  • Company: @CERN

CERN · EPFL'22 alumni · Open-source & Climate

Citation (CITATION.cff) 

cff-version: 1.2.0
message: "If you use this software, please cite it as below."
authors:
- family-names: "Cassayre"
  given-names: "Florian"
  orcid: "https://orcid.org/0000-0001-5784-8051"
title: "A front-end for the LISA proof assistant"
version: 1.0.0
doi: 10.5281/zenodo.6645113
date-released: 2022-06-24
url: "https://github.com/FlorianCassayre/master-project"
license: MIT

GitHub Events

Total
  • Watch event: 1
Last Year
  • Watch event: 1

Committers

Last synced: 9 months ago

All Time
  • Total Commits: 149
  • Total Committers: 1
  • Avg Commits per committer: 149.0
  • Development Distribution Score (DDS): 0.0
Past Year
  • Commits: 0
  • Committers: 0
  • Avg Commits per committer: 0.0
  • Development Distribution Score (DDS): 0.0
Top Committers
Name Email Commits
Florian Cassayre f****e@g****m 149

Issues and Pull Requests

Last synced: 9 months ago

All Time
  • Total issues: 0
  • Total pull requests: 0
  • Average time to close issues: N/A
  • Average time to close pull requests: N/A
  • Total issue authors: 0
  • Total pull request authors: 0
  • Average comments per issue: 0
  • Average comments per pull request: 0
  • Merged pull requests: 0
  • Bot issues: 0
  • Bot pull requests: 0
Past Year
  • Issues: 0
  • Pull requests: 0
  • Average time to close issues: N/A
  • Average time to close pull requests: N/A
  • Issue authors: 0
  • Pull request authors: 0
  • Average comments per issue: 0
  • Average comments per pull request: 0
  • Merged pull requests: 0
  • Bot issues: 0
  • Bot pull requests: 0
View more stats
Top Authors
Issue Authors
Pull Request Authors
Top Labels
Issue Labels
Pull Request Labels