Basic Dafny to PHP Compiler #519
Conversation
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
|
The error message seems a little vague. I think I need to add |
There was a problem hiding this comment.
As discussed offline, this is far too much code to review effectively at once, especially with just a single integration test to assert that it's all correct. I realize the structure of the compiler plugin mechanism makes it challenging to get things off the ground otherwise though. :)
How many of the Compiler methods could you just throw NotImplementedException from? I'd suggest just removing all the code that you copied and modified from other compilers that isn't necessary to have Hello.dfy pass.
|
This is now significantly trimmed down (and hopefully easier to review) @robin-aws. |
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
AWS CodeBuild CI Report
Powered by github-codebuild-logs, available on the AWS Serverless Application Repository |
Significantly better, thanks! It's still a lot but I think we're at the minimum without refactoring the Compiler interface. I think that needs to happen sooner rather than later, and once this is merged I want to scope that out to see if it's reasonable to do before any further work here. |
There was a problem hiding this comment.
Just started adding comments but wanted to send the cause of your build failure first before getting too far. May send a second batch of comments shortly after.
The error message seems a little vague. I think I need to add
php.exeto the build system first.
You're hitting this assertion in IdProtect, which doesn't know about PHP as a compile target yet:
dafny/Source/Dafny/DafnyAst.cs
Line 2940 in d6c53f3
I have no clue how this would have worked on your machine. :) Missing a file?
| public override string TargetLanguage => "PHP"; | ||
|
|
||
| protected override void EmitHeader(Program program, TargetWriter wr) | ||
| { |
There was a problem hiding this comment.
Nit throughout: the standard style in this codebase seems to be same-line open bracket. And hey, that will probably cut another 100 lines or so! :)
| { | ||
| wr.WriteLine("<?php"); | ||
| wr.WriteLine("declare(strict_types=1);"); // Weak-typing in PHP is bad. | ||
| wr.WriteLine("// Dafny program {0} compiled into PHP", program.Name); |
There was a problem hiding this comment.
Is there any way to embed the program text in a way that tooling can extract it from a PHP package?
…piler-php-clean # Conflicts: # Source/Dafny/DafnyPipeline.csproj # Source/DafnyDriver/DafnyDriver.cs # Source/DafnyRuntime/DafnyRuntime.csproj
This successfully compiles Hello.dfy to a valid Hello.php file that executes successfully and produces almost the correct result.
The next step in this effort will be the development of a fleshed out DafnyRuntime.php.