Mill

VerCors' build system is Mill.

TL;DR I'm using sbt, how to make it work again?

• Delete .idea and .bsp;
• Import the VerCors project, if given the choice: as a BSP project;
• This will likely fail the first time (I think due to generated sources), so let it fully finish, then;
• Refresh the project.

That's it! Some common SBT tasks and their replacements:

• compile: The build in IntelliJ instructs mill via BSP to build the project, no settings required anymore. From the command line: ./mill vercors.compile
• reload: not necessary anymore, meta-build definitions such as ColHelper are just normal definitions in mill.
• clean: this now cleans everything completely, I don't think there is a way to clean only a part. However, mill seems to be very conservative with caching when you change the build definition, so it should rarely be necessary to clean the project.

For run configurations: choose the classpath of module "vercors" (as it was with SBT also).

Why mill and not SBT?

In general, see here.

Why not sbt:

• For meta-build alterations in ColHelper, it's annoying to remember that you need to reload
• You need to alter the IntelliJ settings immediately, otherwise the project does not build
• The run script breaks for almost every user, because we use a custom classpath caching solution, because sbt "run example.pvl" starts up way too slow (~7 seconds when vercors is already entirely compiled)
• Most people have encountered a situation where the project just breaks, and you need to re-import everything
• Anything custom is hard to implement, because at least I (Pieter) don't understand enough about how sbt works

Why mill:

• It is almost just scala
• Tasks are a straightforward and easy abstraction:
  • Custom stuff is easy to implement, even when interacting with mill internals
  • Caching is essentially free due to the data model
  • Tooling around mill is easy, because the hierarchy in the build definition corresponds to the hierarchy in out
  • You can chain tasks entirely as you like and mill is fine with it: e.g. col.generatedSources depends on colMeta.meta.runClasspath.
• Mill boots with the vercors build in under one second, e.g. time ./mill -j 0 vercors.classPathArgumentFile -> real 0m0,753s
  • This means we can finally get rid of our own classpath abstraction: we can be sure vercors runs normally every time.
• Mill seems to work well with IntelliJ via the BSP integration, which does not need any altered settings in IntelliJ.

Vercors build structure

Recommended reading:

• Usage, Modules, introspection
• T, T.sources, T.command, and the Cheatsheet for tasks
• $file imports

We split up the build files for two reason: readability, and caching. In principle mill invalidates all target outputs if the build definition is changed, the exception being targets that are defined in a different file. Thus: we extract build definitions that make sense as an abstraction (e.g. project/viper.sc), and tasks that we definitely don't want to repeat vacuously when iteratively tweaking the build (such as download stuff, e.g. project/fetchViper.sc). The root build file picked up by mill and IntelliJ is build.sc, by convention we store all other build files in the project folder.

Definitions that are shared by (nearly) all modules in the build are defined in project/common.sc. Do not put definitions in here that are only relevant to a single module, such as dependency versions: updating those invalidates the entire build. Note that in mill, ScalaModule extends JavaModule, a pattern we observe also. We try to pin a scala version across the vercors modules. VercorsJavaModule inverts the directory structure: sources are not located in moduleName/src, but src/moduleName.

All vercors modules are also "releasable", as defined in project/release.sc. This means that they can be assembled into our preferred output formats, like .deb and .zip. For this we force a distinction between resources: those that are assembled into the giant jar (packedResources) and those that have to remain separate files (bareResources). For module dependencies that are not releasable we assume their resources can be packed into the jar.

You can run vercors normally via ./mill vercors.run a b c, but in this case vercors does not realize it is running in a terminal with ANSI escape code support. To enable nice progress, you can run vercors via ./bin/vct. This calls ./mill vercors.runScript, which generates a file that runs java directly from a script.