CThuleHansen
commented
5 years ago Hi Jamie, Good job! Howcome you have changed the ignore files?
Closed SamieJim closed 11 months ago
CThuleHansen
commented
5 years ago Hi Jamie, Good job! Howcome you have changed the ignore files?
SamieJim
commented
5 years ago Hi Jamie, Good job! Howcome you have changed the ignore files?
Thank you Casper, this was a silly accident made during my first few weeks getting to grips with git, do they all now seem correct?
Luckily for me Leo ran into issues with this when cloning the repo and added them back.
peterwvj
commented
5 years ago Hi Jamie, many thanks for submitting a PR.
Besides the functionality related to the translation itself, the PR introduces several changes which are not needed. In short, your changes/additions should be limited to the following kinds of files:
In consequence all of your changes/additions to .pref, .project, .classpath, .launch, .pdf files should be reverted/removed. In addition, I don't see a reason for changing the .gitignore files. If you revert those changes the .pref, .project, .classpath and .launch files, will be ignored by git. However, since these files are now under version control you would have to tell git not to remove (untrack) them as well.
Detailed feedback/clarifications:
core/codegen/isagen/generatedIRtext/AFieldDeclIR17_IR.txt these should probably be output to the target folder, which is already ignored. As a rule of thumb generated files should never be under version control..gitignore files, which you shouldn't have.Appendices.pdf does not belong in this repository.Creating a Tool for the Translation of VDM-SL to Isabelle HOL.pdf does not belong in this repository. Perhaps we could upload your documents to the documentation repository.core/codegen/isagen/.gitignoreIsaGen main.launch)Once you're done tidying up the PR I'm happy to take a second look.
Hope this helps :)
SamieJim
commented
5 years ago Hi Jamie, many thanks for submitting a PR.
Besides the functionality related to the translation itself, the PR introduces several changes which are not needed. In short, your changes/additions should be limited to the following kinds of files:
- .java files,
- test models (.vdmsl files),
- result files for testing purposes (.result files) and
- Apache Velocity template files (.vm files).
In consequence all of your changes/additions to
.pref,.project,.classpath,.launch,.gitignorefiles. If you revert those changes the.pref,.project,.classpathand.launchfiles, will be ignored by git. However, since these files are now under version control you would have to tell git not to remove (untrack) them as well.Detailed feedback/clarifications:
- Rather than ignoring files such as
core/codegen/isagen/generatedIRtext/AFieldDeclIR17_IR.txtthese should probably be output to thetargetfolder, which is already ignored. As a rule of thumb generated files should never be under version control.- Similarly, you removed something from the
.gitignorefiles, which you shouldn't have.Appendices.pdfdoes not belong in this repository.Creating a Tool for the Translation of VDM-SL to Isabelle HOL.pdfdoes not belong in this repository. Perhaps we could upload your documents to the documentation repository.- Please revert unnecessary white space changes like those made to
core/codegen/isagen/.gitignore- Launch configurations should not be under version control (e.g.
IsaGen main.launch)Once you're done tidying up the PR I'm happy to take a second look.
Hope this helps :)
Hi Peter,
I'll get on this, thank you very much, apologies for the messy PR. Should I close and Re-open after all of this is done?
Best,
Jamie.
peterwvj
commented
5 years ago No need to apologize at all :)
I prefer to keep the PR open as long as we're working on it.
peterwvj
commented
5 years ago This looks much better! Thanks @SamieJim! I did a second pass and some additional issues came up.
Overall I think there are too many unnecessary white space changes, which affect the readability of the code negatively. Generally, this will complicate the reviewing process and merges, which is why we want to avoid this. I have only pointed out some of these issues, so please go over the changes and try to improve the code the best you can.
In short, you only need to change files contained in the core/codegen/isagen folder (or its subfolders). If you're changing files that are not contained in this folder then you must have a good reason for doing so. So if a change can't be properly justified, or it's not needed, then just revert it :)
Specific comments:
.gitattributes and .gitignore files. In .gitattributes, it seems like you removed a newline, please add it back. In .gitignore it seems like you added a newline, please remove it. Also please remove the line saying .launch, which I don't think is needed. So once you have reverted all of these changes both the .gitattributes and .gitignore files will not show up as modified. I know all of this may seem minor, but it will most likely cause annoyances (such as merge conflicts) at a later point, which is why we need to avoid unnecessary changes.externals/pom.xml as well. You're adding a pluginManagement XML tag, which I don't think is needed.System.out.println(...)), which is only done for "debugging" purposes, I think.In addition, I have added a few review comments, which will point you to some specific issues in the code. However, similar issues occur other places, so I suggest you go over all of your changes are try to tidy up the code. Other than that it is starting to look good!
@CThuleHansen is fairly busy at the moment, but I think he will have some time next week to go over the PR.
A first draft of the Isabelle generator, all existing tests pass (50/50) but there are a number of velocity templates that need to be written and a few that need to be adjusted for constructs not included in the current list of tests, future work will add support for an increasing number of constructs. As the majority of results files were written based on the existing translation recipe there may be minor errors in them, however they all seem to be correct.