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.

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

Project file commands don't correctly handle output directories #5988

Open
erniecohen opened this issue Dec 17, 2024 · 0 comments
Open

Project file commands don't correctly handle output directories #5988

erniecohen opened this issue Dec 17, 2024 · 0 comments
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@erniecohen
Copy link

Dafny version

4.9.0

Code to produce this issue

dfyconfig.toml:

includes = ["foo.dfy"] 
excludes = []

[options]
output = "bin/"

foo.dfy:

method {:test} foo() { expect true; }
method main() {}


### Command to run and resulting output

```code
dafny run/build/test dfyconfig.toml

all of these should succeed.

What happened?

dafny run dfyconfig.toml succeeds, but puts output files in the top-level directory, instead of into bin/. build and test get the (long) error below. Changing the dfyconfig.toml option to output = "bin" causes run and build to succeed, but test to fail with the error that it couldn't copy apphost to bin because the destination is a folder rather than a file.

Dafny program verifier finished with 0 verified, 0 errors
Failed to compile C# source code using 'dotnet build /Users/ecohen/Library/CloudStorage/WorkDocsDrive-Documents/projects/verifier/test/bin/.csproj -o /Users/ecohen/Library/CloudStorage/WorkDocsDrive-Documents/projects/verifier/test/bin'. Command output was:
  Determining projects to restore...
/usr/local/share/dotnet/sdk/8.0.303/NuGet.targets(591,5): error MSB4044: The "GetRestoreProjectStyleTask" task was not given a value for the required parameter "MSBuildProjectName". [/Users/ecohen/Library/CloudStorage/WorkDocsDrive-Documents/projects/verifier/test/bin/.csproj]

Build FAILED.

/usr/local/share/dotnet/sdk/8.0.303/NuGet.targets(591,5): error MSB4044: The "GetRestoreProjectStyleTask" task was not given a value for the required parameter "MSBuildProjectName". [/Users/ecohen/Library/CloudStorage/WorkDocsDrive-Documents/projects/verifier/test/bin/.csproj]

What type of operating system are you experiencing the problem on?

Mac

@erniecohen erniecohen added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Dec 17, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Development

No branches or pull requests

1 participant