-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Enable GitHub Actions, set up Maven and include publish scripts
- Loading branch information
1 parent
f2632cc
commit 1cd698c
Showing
5 changed files
with
142 additions
and
20 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
name: CI | ||
|
||
on: [push, pull_request] | ||
|
||
jobs: | ||
build: | ||
runs-on: ubuntu-latest | ||
steps: | ||
- uses: actions/checkout@v3 | ||
with: | ||
submodules: recursive | ||
- name: Set up Java | ||
uses: actions/setup-java@v3 | ||
with: | ||
java-version: 8 | ||
distribution: zulu | ||
- name: Execute tests | ||
run: sbt test |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,31 @@ | ||
name: Release | ||
|
||
on: | ||
release: | ||
types: [created] | ||
|
||
jobs: | ||
release: | ||
runs-on: ubuntu-latest | ||
steps: | ||
- uses: actions/checkout@v3 | ||
with: | ||
submodules: recursive | ||
- name: Set up Java | ||
uses: actions/setup-java@v3 | ||
with: | ||
java-version: 8 | ||
distribution: zulu | ||
- name: Execute tests | ||
run: sbt test | ||
- name: Create artifacts | ||
run: sbt publish | ||
- name: Publish artifacts | ||
uses: burnett01/[email protected] | ||
with: | ||
switches: -avzr | ||
path: releases/ | ||
remote_path: maven | ||
remote_host: maven.cassayre.me | ||
remote_user: github | ||
remote_key: ${{ secrets.DEPLOY_KEY }} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -2,3 +2,4 @@ | |
.idea | ||
target | ||
.bsp | ||
releases |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -3,18 +3,76 @@ | |
This repository hosts the work related to my Master Project (PDM) at [LARA](https://lara.epfl.ch/w/). | ||
This includes source code, writeup and any other significant resource related to the project. | ||
|
||
Original project title: ***Automation for Proof Assistant*** | ||
Project title: ***A Proof System for LISA*** | ||
|
||
Dates: **21.02.2022** to **24.06.2022** | ||
|
||
Tentative content: | ||
Content: | ||
In this project I will be working on a proof assistant ([LISA](https://github.com/epfl-lara/lisa)), | ||
in particular I will be designing a higher-level interface to represent and write proofs. | ||
|
||
## Compilation and execution | ||
## Installation as a library | ||
|
||
The Scala project depends on LISA (included as a git submodule) and runs on the same | ||
version to avoid problems. The relevant commands are: | ||
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. | ||
|
||
<details> | ||
<summary>Installing LISA</summary> | ||
|
||
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: | ||
|
||
* **git repository or submodule**: | ||
* If your project **is already** a git repository, then you can add LISA as a submodule: | ||
``` | ||
git submodule add [email protected]: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 [email protected]:epfl-lara/lisa.git | ||
cd lisa | ||
git checkout $COMMIT | ||
cd .. | ||
``` | ||
* **sbt managed dependency**: | ||
* 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) | ||
``` | ||
The table below indicates the version compatibility (= value of `$COMMIT`): | ||
| `master-project` | `lisa` | | ||
|:----------------:|:------------------------------------------:| | ||
| `0.1` | `eacb9c06aa2975b9ae2bc993847c597eb3c54995` | | ||
</details> | ||
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.1" | ||
``` | ||
|
||
## Development | ||
|
||
The Scala project depends on LISA, included as a git submodule: | ||
make sure to run `git submodule update --init --recursive` the first time. | ||
It runs on the same Scala/sbt versions as LISA to avoid problems. | ||
|
||
The relevant commands are: | ||
|
||
* `sbt test` to run the tests | ||
|
||
|
@@ -33,6 +91,12 @@ version to avoid problems. The relevant commands are: | |
git commit lisa | ||
``` | ||
|
||
(make sure to rebuild the entire project after that, to avoid potential issues with incremental compilation) | ||
(make sure to rebuild the entire project after this operation, to avoid potential issues with incremental compilation) | ||
|
||
</details> | ||
|
||
## Licensing | ||
|
||
This project is licensed under the _MIT License_. | ||
|
||
LISA is licensed under the _Apache License 2.0_. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,17 +1,25 @@ | ||
name := "master-project" | ||
lazy val root = (project in file(".")) | ||
.settings( | ||
commonSettings, | ||
name := "master-project", | ||
organization := "me.cassayre.florian", | ||
version := "0.1.0", | ||
versionScheme := Some("semver-spec"), | ||
scalaVersion := "3.1.1", | ||
scalacOptions ++= Seq( | ||
"-feature", | ||
"-language:implicitConversions" | ||
), | ||
libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "2.1.1", | ||
libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test", | ||
) | ||
.dependsOn(lisa) | ||
|
||
version := "0.1" | ||
lazy val lisa = (project in file("lisa")).settings(commonSettings) | ||
|
||
scalaVersion := "3.1.1" | ||
|
||
scalacOptions ++= Seq( | ||
"-feature", | ||
"-language:implicitConversions" | ||
lazy val commonSettings = Seq( | ||
publishTo := Some(MavenCache("local-maven", file("releases"))), | ||
Compile / packageDoc / publishArtifact := false, | ||
//packageDoc / publishArtifact := false, | ||
Compile / doc / sources := Seq.empty, | ||
) | ||
|
||
lazy val lisa = RootProject(file("lisa")) | ||
lazy val root = (project in file(".")).dependsOn(lisa) | ||
|
||
libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "2.1.1" | ||
|
||
libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test" |