Can the leon library be published as a maven artifact?

[NicolasRouquette]

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...)

[NicolasRouquette]

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.