-
Notifications
You must be signed in to change notification settings - Fork 143
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
After discussion with Heiko Becker.
- Loading branch information
Showing
382 changed files
with
0 additions
and
58,433 deletions.
There are no files selected for viewing
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
Oops, something went wrong.
dc68c31
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The CI test failure shows that there are duplicated exported theorems in
examples/logic/foltypesScript.sml
.I think it's possible that previously in
src/parallel_builds/core/Holmakefile
not only "lassie" but also some (if not all) example folders after it were also disabled by the leading "#" character (if the ending backslash is interpreted by unconditionally appending the next line). Now,examples/logic
finally got a chance to run, and the issue is exposed ...dc68c31
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If doing line-commenting (by a leading
#
) in a line ofHolmakefile
with backslash at the end of that line actually means commenting also the next line (or next lines if they also end with backslash), perhaps this behavior should be considered problematic and fixed in the code handlingHolmakefile
.dc68c31
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Indeed! I will check to see what traditional
make
does in this situation.dc68c31
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This reference suggests that what
Holmake
is doing is consistent with established practice.dc68c31
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I see... So
Holmake
behaves correctly.