Closed keyboardDrummer closed 1 year ago
Why is #2906 a prerequisite? I would think if anything it would be in the other direction, and even then that the first version of dafny server
could just accept the same style of CLI arguments as other dafny
commands at first.
Some notes on requirements and scoping down the initial version of this:
--no-verify
for example, should remain a CLI option for a particular command invocation context. You shouldn't be able to say "this project is configured to never be verified". dafny report
command in the future.build.gradle.kts
files?
Additional features that will be nice to add AFTER the first version:
Program
for the Dafny pipeline, and control the name of (for example) the DLL file dafny build
produces (instead of taking the name of the first source file)--library
flag as-is, but will likely need something different in the future.If we went along the route of defining a build file in Dafny, it could be great to get inspired by Mill if we went the route of having the project file defined in Dafny - which I think is an excellent idea. But Dafny lacks reflection that would be useful for a build tool. I was using Mill even for Non-scala projects because it was so good at caching intermediate step.
However, as @robin-aws , I think it would be good to reduce the scope of the project to something manageable for now.
Enable specifying options to the Dafny CLI in a Dafny project file, which can be passed as an argument when calling the Dafny CLI, also when using the
dafny server
command.
There's three pieces of work:
dafny server
commanddafny server
command, which doesn't take input files, to locate Dafny project files for the .dfy files that it's analysing, by traversing up the file tree.(3) depends on (1) and (2), and I scoped this issue to be (2) and (3), so it depends on (1). However, feel free to scope (3) into a separate issue and to consider this issue being just (2).
Adding list of Dafny command and arguments which I think are relevant for project file : added value types for my understanding. 1) Resolve :
2) verify :
3) Translate :
4) Audit :
Again I would argue that we should not check options both in parsing a project file and in using it in the CLI. To do so means that any change to options requires maintenance in two places, rather than one, and gives no particular benefit to the user.
Keep it simple. Keep it user-editable. To me a flat file with options and values would be just fine.
List looks alright. I don't think it needs to be perfect in one go. You might even allow everything at first and see how that goes.
I think you're general strategy might be:
Remember that a primary reason for the project file is to list the dependent files, more than the options per se. SO the UX for that use case has to be great.
Again I would argue that we should not check options both in parsing a project file and in using it in the CLI. To do so means that any change to options requires maintenance in two places, rather than one, and gives no particular benefit to the user.
Keep it simple. Keep it user-editable. To me a flat file with options and values would be just fine.
A flat file would provide some benefit, but a project file is much more useful with some awareness of what options apply to which commands. If you want to --include-runtime
when translating your project, for example, you can't just pass that flag to every command you run, because dafny verify --include-runtime ...
is rejected, for example.
This is perhaps the difference between a project file and a file with a convenient batch of options to make CLI commands shorter. Personally when I feel the need for the latter, I make a shell script wrapper that prepends/appends common arguments instead, so I don't consider that a hard requirement. If the project file has a [common]
section, though, you could use that for any options that are accepted by all commands (or at least all the ones you ever run :)
I do share the concern over the maintenance burden though. It would be technically possible to allow any options in a project file and just drop any that aren't supported by the current command, but then you're at risk of silently dropping a critical option. I can at least imagine an implementation strategy where we have project file sections that line up one-to-one with command and common property bags to make it easier.
Remember that a primary reason for the project file is to list the dependent files, more than the options per se. SO the UX for that use case has to be great.
Absolutely, but we should be able to provide some incremental benefit by leaning on using --library
as an option instead for now. I expect when we have a clearer idea of the nature of a Dafny package/dependency, we should be able to add a dedicated dependencies section.
Problems
Make
or a Bash script to enable easily invoking the Dafny CLI.Prerequisites
Out of scope
Solution
Enable specifying options to the Dafny CLI in a Dafny project file, which can be passed as an argument when calling the Dafny CLI, also when using the
dafny server
command.