From 6b1b18efe8ac572d6b1c70ba318a3821dacbfca2 Mon Sep 17 00:00:00 2001 From: Sankalp Gambhir Date: Fri, 17 Jan 2025 11:44:57 +0100 Subject: [PATCH 1/4] Move lisa examples into proper a package --- .../src/main/scala/{ => lisa/examples}/ADTExample.scala | 2 ++ lisa-examples/src/main/scala/{ => lisa/examples}/Example.scala | 2 ++ .../src/main/scala/{ => lisa/examples}/ExampleKernel.scala | 2 ++ lisa-examples/src/main/scala/{ => lisa/examples}/Lattices.scala | 2 ++ 4 files changed, 8 insertions(+) rename lisa-examples/src/main/scala/{ => lisa/examples}/ADTExample.scala (99%) rename lisa-examples/src/main/scala/{ => lisa/examples}/Example.scala (99%) rename lisa-examples/src/main/scala/{ => lisa/examples}/ExampleKernel.scala (97%) rename lisa-examples/src/main/scala/{ => lisa/examples}/Lattices.scala (99%) diff --git a/lisa-examples/src/main/scala/ADTExample.scala b/lisa-examples/src/main/scala/lisa/examples/ADTExample.scala similarity index 99% rename from lisa-examples/src/main/scala/ADTExample.scala rename to lisa-examples/src/main/scala/lisa/examples/ADTExample.scala index 77b8abc75..f9ce19e3a 100644 --- a/lisa-examples/src/main/scala/ADTExample.scala +++ b/lisa-examples/src/main/scala/lisa/examples/ADTExample.scala @@ -1,3 +1,5 @@ +package lisa.examples + object ADTExample extends lisa.Main { import lisa.maths.settheory.types.adt.{*, given} diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/lisa/examples/Example.scala similarity index 99% rename from lisa-examples/src/main/scala/Example.scala rename to lisa-examples/src/main/scala/lisa/examples/Example.scala index 494964d9c..e27314e94 100644 --- a/lisa-examples/src/main/scala/Example.scala +++ b/lisa-examples/src/main/scala/lisa/examples/Example.scala @@ -1,3 +1,5 @@ +package lisa.examples + import lisa.automation.Congruence import lisa.automation.Substitution.{ApplyRules as Substitute} import lisa.automation.Tableau diff --git a/lisa-examples/src/main/scala/ExampleKernel.scala b/lisa-examples/src/main/scala/lisa/examples/ExampleKernel.scala similarity index 97% rename from lisa-examples/src/main/scala/ExampleKernel.scala rename to lisa-examples/src/main/scala/lisa/examples/ExampleKernel.scala index 9fa6dce86..86b457eb9 100644 --- a/lisa-examples/src/main/scala/ExampleKernel.scala +++ b/lisa-examples/src/main/scala/lisa/examples/ExampleKernel.scala @@ -1,3 +1,5 @@ +package lisa.examples + import lisa.utils.K import K.* diff --git a/lisa-examples/src/main/scala/Lattices.scala b/lisa-examples/src/main/scala/lisa/examples/Lattices.scala similarity index 99% rename from lisa-examples/src/main/scala/Lattices.scala rename to lisa-examples/src/main/scala/lisa/examples/Lattices.scala index cbc4c28ed..4bb2286c0 100644 --- a/lisa-examples/src/main/scala/Lattices.scala +++ b/lisa-examples/src/main/scala/lisa/examples/Lattices.scala @@ -1,3 +1,5 @@ +package lisa.examples + object Lattices extends lisa.Main { val x = variable From 25bd25b4d191430781c3a45eaea24bd1fffb157e Mon Sep 17 00:00:00 2001 From: Sankalp Gambhir Date: Fri, 17 Jan 2025 11:45:11 +0100 Subject: [PATCH 2/4] Remove infix method warning --- .../src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala b/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala index d9a2cd984..9504fa11d 100644 --- a/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala +++ b/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala @@ -128,7 +128,7 @@ object SimpleDeducedSteps { */ val newStep = K.SCSubproof(K.SCProof(IndexedSeq(p0, p1, p2), IndexedSeq(p.conclusion)), Seq(p.length - 1)) ( - p withNewSteps IndexedSeq(newStep), + p.withNewSteps(IndexedSeq(newStep)), in, j ) From 40cf77d5e48b9b64d2a8f80a0b1f393c7df15103 Mon Sep 17 00:00:00 2001 From: Sankalp Gambhir Date: Fri, 17 Jan 2025 11:45:24 +0100 Subject: [PATCH 3/4] Add metals and mill files to gitignore --- .gitignore | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.gitignore b/.gitignore index aaadedc95..5b1158349 100644 --- a/.gitignore +++ b/.gitignore @@ -2,12 +2,12 @@ .idea .metals .vscode -project/metals.sbt -project/project/metals.sbt +metals.sbt sbt-launch.jar # build-related .bsp +out/ .bloop target *.scala.semanticdb From 4258187045446245c574c53963929f5e0f3aa92a Mon Sep 17 00:00:00 2001 From: Sankalp Gambhir Date: Fri, 17 Jan 2025 12:46:33 +0100 Subject: [PATCH 4/4] Add mill build --- build.mill | 127 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 127 insertions(+) create mode 100644 build.mill diff --git a/build.mill b/build.mill new file mode 100644 index 000000000..e73e95b80 --- /dev/null +++ b/build.mill @@ -0,0 +1,127 @@ +package build + +import mill._ +import scalalib._, scalajslib._ +import publish._ + +object Configuration { + val version = "0.7" + val scala2Version = "2.13.8" + val scala3Version = "3.5.2" +} + +import utilities._ + +trait LisaRootModule extends PublishModule with LisaModule with CrossScalaModule { + def publishVersion = Configuration.version + + def pomSettings = PomSettings( + description = artifactName(), + organization = "ch.epfl.lara", + url = "https://github.com/epfl-lara/lisa", + licenses = Seq(License.`Apache-2.0`), + versionControl = VersionControl.github(owner = "epfl-lara", repo = "lisa"), + developers = Seq( + Developer("SimonGuilloud", "Simon Guilloud", "https://github.com/SimonGuilloud"), + Developer("sankalpgambhir", "Sankalp Gambhir", "https://github.com/sankalpgambhir"), + Developer("vkuncak", "Viktor Kuncak", "https://github.com/vkuncak"), + Developer("agilot", "Andrea Gilot", "https://github.com/agilot"), + ) + ) +} + +object lisa extends Module { + + def scalaVersions = Seq(Configuration.scala3Version) + + object jvm extends Cross[JvmLisaModule](scalaVersions) + trait JvmLisaModule extends LisaRootModule with ScalaModule { + object test extends LisaTests with ScalaTests + } + + object js extends Cross[JsLisaModule](scalaVersions) + trait JsLisaModule extends LisaRootModule with ScalaJSModule { + def scalaJSVersion = "1.16.0" + object test extends LisaTests with ScalaJSTests + } +} + +trait LisaModule extends ScalaModule { + + def jarDeps = Agg.empty[JarDep] + + override def unmanagedClasspath = Task { + jarDeps.map( jar => { + val JarDep(name, uri) = jar + val path = Task.dest / s"$name.jar" + os.write(path, requests.get.stream(uri)) + PathRef(path) + } + ) + } + + def scalacOptions = Seq( + "-feature", // list all feature warnings + "-language:implicitConversions", // universally enable implicit conversions + "-Wconf:msg=.*will never be selected.*:silent", // spurious resolution warnings + ) + + trait LisaTests extends ScalaTests with TestModule.Utest +} + +trait Scala3Module extends ScalaModule { + def scalaVersion = Configuration.scala3Version +} + +object `lisa-kernel` extends LisaModule with Scala3Module + +object `lisa-utils` extends LisaModule with Scala3Module { + + def moduleDeps = Seq(`lisa-kernel`) + + override def jarDeps = Agg( + jar"ch.epfl.lara::scallion:0.6" from "https://github.com/epfl-lara/scallion/releases/download/v0.6/scallion_3-0.6.jar", + jar"ch.epfl.lara::silex:0.6" from "https://github.com/epfl-lara/silex/releases/download/v0.6/silex_3-0.6.jar", + jar"io.github.leoprover::scala-tptp-parser:0.2" from "https://github.com/SimonGuilloud/scala-tptp-parser/releases/download/v0.2/scala-tptp-parser_2.13-0.2.0.jar", + ) + + override def ivyDeps = Agg( + ivy"org.scalatest::scalatest:3.2.18", + ivy"com.lihaoyi::sourcecode:0.4.2", + ) + +} + +object `lisa-sets` extends LisaModule with Scala3Module { + def moduleDeps = Seq( + `lisa-kernel`, + `lisa-utils`, + ) +} + +object `lisa-examples` extends LisaModule with Scala3Module { + def moduleDeps = Seq( + `lisa-kernel`, + `lisa-utils`, + `lisa-sets`, + ) +} + +object utilities { + + case class JarDep(artifact: String, uri: String) + + case class JarConstructor(artifact: String) { + def from(uri: String): JarDep = { + JarDep(artifact, uri) + } + } + + implicit class JarWrapper(val sc: StringContext) { + def jar(parts: String*): JarConstructor = { + val artifactRaw = sc.s(parts: _*) + val artifact = artifactRaw.replace(':', '_') // ':' in jar name breaks class resolution + JarConstructor(artifact) + } + } +}