Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

dafny run should support project files #4622

Closed
fzaiser opened this issue Oct 5, 2023 · 0 comments · Fixed by #4629
Closed

dafny run should support project files #4622

fzaiser opened this issue Oct 5, 2023 · 0 comments · Fixed by #4629
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny

Comments

@fzaiser
Copy link

fzaiser commented Oct 5, 2023 •
edited
Loading

Summary

Most Dafny commands support project files (e.g. dafny server, dafny build, dafny test). For consistency, dafny run should support it too.

Background and Motivation

Using a project file has many advantages, such as not having to write includes. For VMC, we're using a project file and thus would like to get rid of includes. But we also want to use dafny run in CI, which does not support project files:

$ dafny run dfyconfig.toml
*** Error: 'dfyconfig.toml': Filename extension '.toml' is not supported. Input files must be Dafny programs (.dfy) or supported auxiliary files (.cs, .dll)
$ dafny run Main.dfy --input dfyconfig.toml
*** Error: 'dfyconfig.toml': Filename extension '.toml' is not supported. Input files must be Dafny programs (.dfy) or supported auxiliary files (.cs, .dll)

Solving this issue would be very helpful for us.

Proposed Feature

dafny run should accept a *.toml project file like dafny build and dafny test.

Alternatives

No response
@fzaiser fzaiser added the kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny label Oct 5, 2023
@fzaiser fzaiser mentioned this issue Oct 6, 2023
Closed
@keyboardDrummer keyboardDrummer mentioned this issue Oct 9, 2023
Merged
keyboardDrummer added a commit that referenced this issue Oct 11, 2023
@keyboardDrummer
Enable passing project files to 'dafny run' (#4629)
9f4dd59 
Fixes #4622

### Description
- Enable passing project files to 'dafny run'
- Add a hidden `--build` option to configure where intermediate build
files are placed when using `dafny run`

### How has this been tested?
Added a littish test

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
robin-aws pushed a commit to robin-aws/dafny that referenced this issue Oct 11, 2023
@keyboardDrummer @robin-aws
Enable passing project files to 'dafny run' (dafny-lang#4629)
6c4931e 
Fixes dafny-lang#4622

### Description
- Enable passing project files to 'dafny run'
- Add a hidden `--build` option to configure where intermediate build
files are placed when using `dafny run`

### How has this been tested?
Added a littish test

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
robin-aws pushed a commit to robin-aws/dafny that referenced this issue Oct 13, 2023
@keyboardDrummer @robin-aws
Enable passing project files to 'dafny run' (dafny-lang#4629)
2a00111 
Fixes dafny-lang#4622

### Description
- Enable passing project files to 'dafny run'
- Add a hidden `--build` option to configure where intermediate build
files are placed when using `dafny run`

### How has this been tested?
Added a littish test

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Enable passing project files to 'dafny run' keyboardDrummer/dafny
1 participant
@fzaiser