dafny test and --output option

[DavePearce]

Summary

(This is related to #3611)

Unlike dafny build, the dafny test command does not support the --output option. When run with the --target java option it just dumps the generated java files into the directory where the file being tested is contained (in my case src/dafny directory). This is not an ideal place to store generate files, and it would be nice to have some control here.

Background and Motivation

I'm trying to update by project build file to use the new CLI syntax (e.g. dafny build, etc).

Proposed Feature

Adding --output as an option for dafny test.

Alternatives

No response

[keyboardDrummer]

How would you feel about the generated files being placed in a temporary directory by default for dafny test and dafny run ? The generated files don't seem particularly relevant for either of these commands.

Also, should the default value of --output be something like output or build ?

[hmijail]

One use case for controlling the output in all cases is for build pipelines. If the build product exists and is newer than the sources then we know we don't need to rebuild/retest.

[DavePearce]

How would you feel about the generated files being placed in a temporary directory by default for dafny test and dafny run

Well, in essence that's what its doing now isn't? Or do you mean an OS-generated temporary directory (e.g. in /tmp/ on UNIX systems)? I think that would be sensible. Eitherway, as long as I can control where they go, then that is enough.

[keyboardDrummer]

Or do you mean an OS-generated temporary directory (e.g. in /tmp/ on UNIX systems)?

Yes that's what I meant, with the purpose of not letting these temporary files pollute the user's file space.

Eitherway, as long as I can control where they go, then that is enough.

Do you need to control it for run and test, if the files don't get in your way?

[DavePearce]

Do you need to control it for run and test, if the files don't get in your way?

Hmmmm, well I feel like control is always a good thing. For example, if I want to compile directly against an external dependency. Whilst I did successfully work around that by using an interface with a default implementation for Dafny to compile against, this didn't feel like a great solution.

[keyboardDrummer]

Hmmmm, well I feel like control is always a good thing. For example, if I want to compile directly against an external dependency.

If you want to use dafny run with an external dependency, then you have to pass that on the CLI, like dafny run myDafnySource.dfy myDotNetDependency.dll. In this case, why do you want control over where intermediate .dll files are placed?

[DavePearce]

If you want to use dafny run with an external dependency, then you have to pass that on the CLI,

Hmmm, so I could pass a jar file on the command-line then? I guess that works. Generally speaking though, when working with a build system (e.g. Maven, Gradle, Cargo, etc) you have a directory where generated files get placed (e.g. bin, target, etc). Being able to specify where the temporary files go is consistent with that. It means, for example, I can always clean that directory up. It also means I can inspect the actual generated code easily enough if I want to, etc. Otherwise, I have to go digging to figure out where Dafny placed the temporary files if I need to debug them. Also, if Dafny crashes for some reason, it may not clean up the temporary files, etc.

Anyway, we're probably getting side tracked. Using a temporary directory for the intermediate files resolves the main issue. Whether or not you choose to support --output I guess is a secondary thing. Like I said, control is always a good thing IMHO.

[keyboardDrummer]

Generally speaking though, when working with a build system (e.g. Maven, Gradle, Cargo, etc) you have a directory where generated files get placed (e.g. bin, target, etc). Being able to specify where the temporary files go is consistent with that. It means, for example, I can always clean that directory up. It also means I can inspect the actual generated code easily enough if I want to, etc. Otherwise, I have to go digging to figure out where Dafny placed the temporary files if I need to debug them. Also, if Dafny crashes for some reason, it may not clean up the temporary files, etc.

Makes sense. Thanks for adding this!

I also wonder whether we want to distinguish between output files and intermediate build files.

dafny run / dafny test: there are only intermediate build files
dafny build: there are intermediate build files, and one output file (although it might be good to plan for multiple output files)
dafny translate: there are no intermediate build files, and one or multiple output files

Does it makes sense to have a separate intermediate and output folder? Also, I'm thinking it might be better to keep the intermediate build artifacts around, for possible caching purposes, although that raises the question of when to delete them.

Also, I'm wondering to what extend we should allow different commands to overwrite each other's outputs. Suppose you do dafny translate followed by some code changes and then dafny run, do you expect the translated files to stay the same?

How would a default directory structure like:

projectRoot
  src
  output
    cache (would contain the intermediate files, so you could inspect those by looking here)
    build
    translate

be?

This would imply two options:
--cache: available for most commands, defaults to ./output/cache
--output: available for build and translate, defaults to ./output/<commandName>