Fix 4922 #4923
Fix 4922 #4923
Conversation
|
Hello all, this is my first PR for this repo. I would especially appreciate feedback on the naming I used for variables and options. Additionally, I am not very familiar with Java, and I haven't modified that backend to take advantage of the new option. After initial reviews and settling on naming, etc. I will update release notes. |
| @@ -255,6 +255,7 @@ public enum ContractTestingMode { | |||
| public bool FormatCheck = false; | |||
|
|
|||
| public string CompilerName; | |||
| public string CompilerExecutable = null; | |||
There was a problem hiding this comment.
Could you remove this field and instead refer to this variable using the expression options.Get(CommonOptionBag.TargetExecPath) ?
There was a problem hiding this comment.
Amazing! Thanks a lot.
I don't see any tests for the --target-executable option you added. Could you add some or any littish tests for this? You can look in the folder Source/IntegrationTests/TestFiles/LitTests/LitTest/cli for inspiration.
Also, one thing that I find curious is that our current integration tests, which also run on Windows, and which also run Dafny code using the Python back-end, already pass. It seems that python3 is available on the path of our Windows integration test machine. I wonder whether we do anything to make that available (it seems not), and if so if we should remove that workaround. @alex-chew @MikaelMayer @robin-aws any idea why this is currently working?
Also, as described this PR fixes #4922, but it also adds the option --target-executable (which I see is also mentioned in the issue description, but I would consider it a separate thing). Adding that in the details would have made the review slighty easier.
| @@ -151,12 +151,19 @@ public enum AssertionShowMode { None, Implicit, All } | |||
| java - Compile to Java. | |||
| py - Compile to Python. | |||
| cpp - Compile to C++. | |||
| rs - Compile to Rust. | |||
There was a problem hiding this comment.
Rust is not a fully supported target at this point, so I'm not sure this line should be here. I'd prefer removing it.
There was a problem hiding this comment.
Perhaps adding [EXPERIMENTAL] ? Removing it from the list seems improper since it is technically an available option. I'll remove it still if you'd like, but just wanted to offer that as point.
There was a problem hiding this comment.
OK, that suggestion works for me !
|
|
||
| Note that the C++ backend has various limitations (see Docs/Compilation/Cpp.md). This includes lack of support for BigIntegers (aka int), most higher order functions, and advanced features like traits or co-inductive types.".TrimStart() | ||
| ) { | ||
| ArgumentHelpName = "language", | ||
| }; | ||
|
|
||
| public static readonly Option<string> TargetExecPath = new(new[] { "--target-executable", "-T" }, @" |
There was a problem hiding this comment.
I find the term executable ambiguous in this context. Executable for what? Filename of the executable we generate when using dafny build ? Executable used to downstream compile the translated target language code? Executable used to run the translated code or downstream artifacts?
Based on the code I think this is only used to execute code for that target, so something like target-runtime target-execution-runtime or target-execution-binary might be more specific.
There was a problem hiding this comment.
Thank you for this feedback! This is exactly what I was unsure about. For C and Rust , it's the compiler. For Python and Javascript, it's the interpreter. For Java though, there are three different executables that get called after translation before it gets run. I typically like to err on the side of explicitness. I agree about the ambiguity, it hasn't sat right with me at all lol.
- For Python and Javascript, it's an "interpreter"
- For C++ and Rust, it's a compiler
- For Java, it's a compiler and runtime
- For C#, it's also a compiler and runtime, but only presented as a compiler.
There was a problem hiding this comment.
I think for Java you haven't updated the back-end, so the option has no effect. For C# the option is used to choose the binary that runs an already produced .dll, so I would consider it being used as a runtime.
To be frank, I think it's better not to have the --target-executable option. For a particular back-end, we can't assume anything about what tools it relates to. Dafny might also have a native back-end that produces a binary and requires no further tools.
I think what we potentially do want is to be able to tell Dafny where the locations of particular tools are, such as where is dotnet, where is the python interpreter, etc. Whether this should be done through Dafny CLI options, through environment variables, or through some sort of machine scoped Dafny configuration, I'm not sure. I'm reluctant to use Dafny CLI options for this since it would lead to significant bloat in commands that are by default target-agnostic: dafny run and dafny build are intended for Dafny applications and libraries that don't integrate in a larger non-Dafny applications.
There was a problem hiding this comment.
I think I can see your reasoning. I also agree with the concern for CLI bloat. I think what I have put forth so far might be a little off the mark. Additionally, I think I should split this PR to be more targeted, scope-wise. I will split out the CLI and associated code changes, leaving only the changes related to the python executable.
As far as the purpose of dafny run and dafny build, I think it may be helpful to clarify in the available documentation their purpose. That being said, I am an outsider for this repository and language, but I think the inclusion of the --target option leaves a hole between the possible and intended use cases without some kind of further modifications, in line with your 3rd paragraph. The hole is that I can run the code using a target language, but I have no control over how it actually gets run. This leaves a bit of a functional conundrum as the --target option already implies that the user wants some control over how things happen, but the only control the user really gets is "language", which most users who care about language would likely already be familiar with the footguns associated with not being able to target versions or other options of that language.
Again, I'm a bit of a newcomer, but I believe this warrants additional discussion that I am happy to contribute to and can open a new issue to facilitate that discussion. In the mean time, I will re-scope the changes in this PR to allow the initial issue to be resolved without the other can of worms I seem to have opened :P
There was a problem hiding this comment.
Again, I'm a bit of a newcomer, but I believe this warrants additional discussion that I am happy to contribute to and can open a new issue to facilitate that discussion.
It does warrant it! Thank you for opening that issue.
Will do!
Thank you for this feedback, I will keep it in mind for the future. |
|
Closing in lieu of more targeted PR. |
Description
Fixes #4922
How has this been tested?
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.