Open NicolasRouquette opened 7 years ago
I see that there's a bit of a problem w.r.t. publishing the leon library.
First, the build.sbt defines a source code generator for a leon/Build.scala
file that has the absolute path of the leon project directory (leon.Build.baseDirectory
) and the list of the absolute path for each source file in the leon library (leon.Build.libFiles
).
Second, according to the latest commit, 57fc12d, there are 5 different places where the organization of the leon.Build
generated source is used:
1) In leon.Main, there is a watcher for continuously monitoring changes in the leon library in addition to the source files specified on the command line.
2) In leon.frontends.scalac.ClassgenPhase, all the leon library sources files are added to all the source files specified on the command line as compiler options.
3) In leon.frontends.scalac.CodeExtraction, there is a predicate, isLIbrary to check whether a particular source file belongs to the leon library.
4) In leon.frontends.scalac.ExtractionPhase, all the leon library sources files are added to all the source files specified on the command line as compiler options
5) In leon.test.LeonRegressionSuite, the helper function filesInResourceDir uses the Build.baseDirectory
as the starting point for searching for regression test resource files.
I propose to refactor leon
to do away with hardcoded locations in leon.Build
. Without this, publishing a leon.jar
artifact looses a lot of utility because because a user who doesn't have the leon
project cloned in the same location as leon.Build.baseDirectory
would have to clone leon
anyway and include on the command line all of the leon
library source files.
There is a simple solution to this:
Include the leon
library as resources
copy leon/library/leon/*
to leon/src/main/resources/leon/
For the first 4 usages of leon.Build
above, add a new command-line option to specify where to get the leon
library:
Specify a path to a leon
library base directory. This is effectively equivalent to ${leon.Build.baseDirectory}/library/**/*.scala
currently without this base directory being hardcoded.
Extract the leon
library from the leon.jar
resource to a temporary directory and use that as the path the the leon
library base directory per the above. This case could be the default behavior, which would be effectively equivalent to the current behavior except that a user wouldn't have to clone leon
& publish it locally.
For the 5th usage, it is sufficient to resolve the regressionTestDirectory from the LeonRegressionSuite
's class loader.
Is it possible to publish the leon library as a maven jar with sources such that one could write scala code with a dependency on the leon library maven jar/source and use leon to analyze such source code? (verification, synthesis, etc...)