cross-platform I/Q Makefile#233
Conversation
hanno-becker
left a comment
hanno-becker
left a comment
There was a problem hiding this comment.
Thank you @edoput! I tested it on Mac and Linux and it works. One should error out early if the Isabelle binary is not found, but this can be follow-up.
|
The CI failures in |
hanno-becker
left a comment
hanno-becker
left a comment
There was a problem hiding this comment.
On second look, noted a probably unintentional change in the scala flags. Can you restore the original, and while at it also add a check if the Isabelle binary has been found, and otherwise nudge the user to set ISABELLE_HOME appropriately?
edoput
force-pushed
the
main
branch
2 times, most recently
from
a73567b to
071d244
Compare
edoput
force-pushed
the
main
branch
3 times, most recently
from
3926efc to
e9a9ad3
Compare
| ISABELLE_BIN ?= $(if $(wildcard $(ISABELLE_HOME)/bin/isabelle),$(ISABELLE_HOME)/bin/isabelle,isabelle) | ||
| ifeq ($(wildcard $(ISABELLE_BIN)),) | ||
| $(error Isabelle binary not found at $(ISABELLE_BIN). \ | ||
| Set ISABELLE_HOME correctly, e.g. make ISABELLE_HOME=/path/to/Isabelle/bin) |
There was a problem hiding this comment.
ISABELLE_HOME is assumed to be the root directory here, not bin
| ZSTD_JAR := $(firstword $(wildcard $(ISABELLE_HOME)/contrib/zstd-jni-*/lib/zstd-jni-*.jar)) | ||
| ISABELLE_JAR ?= $(ISABELLE_HOME)/lib/classes/isabelle.jar | ||
| JAVA_HOME ?= $(shell $(ISABELLE) getenv -b JAVA_HOME 2>/dev/null) | ||
| ISABELLE_BIN ?= $(if $(wildcard $(ISABELLE_HOME)/bin/isabelle),$(ISABELLE_HOME)/bin/isabelle,isabelle) |
There was a problem hiding this comment.
This renames $ISABELLE to $ISABELLE_BIN but does not adjust all usages, specifically make test below.
hanno-becker
left a comment
hanno-becker
left a comment
There was a problem hiding this comment.
Two minor issues still need fixing, see comments
|
I should have addressed the last issues. The isabelle binary is only addressed using ISABELLE_BIN and I have introduced a check that it is a real command. In the test command ISABELLE was only used in one test. While the rest of the recipe uses a different pattern. Which one is appropriate and should be kept? |
| ifeq ($(shell command -v "$(ISABELLE_BIN)" > /dev/null 2>&1 && echo yes),) | ||
| $(error Isabelle binary not found or not executable at $(ISABELLE_BIN). \ | ||
| Set ISABELLE_HOME correctly, e.g. make ISABELLE_HOME=/path/to/Isabelle, or ensure | ||
| 'isabelle' is in your PATH) | ||
| endif |
There was a problem hiding this comment.
Apologies for not thinking of this earlier, but this will prevent a plain make help if you haven't yet figured out the ISABELLE_HOME.
Consider this:
# Verify Isabelle binary is available (only required for build/test/install)
.PHONY: check-isabelle
check-isabelle:
@command -v "$(ISABELLE_BIN)" > /dev/null 2>&1 || { \
echo "Error: Isabelle binary not found or not executable at $(ISABELLE_BIN)." >&2; \
echo "Set ISABELLE_HOME correctly, e.g. make ISABELLE_HOME=/path/to/Isabelle," >&2; \
echo "or ensure 'isabelle' is in your PATH." >&2; \
echo "Run 'make help' for more information." >&2; \
exit 1; \
}
and then add check-isabelle to the targets that actually run Isabelle.
| JAVA_HOME="$(JAVA_HOME)" PATH="$(JAVA_HOME)/bin:$$PATH" cd $(CLASSES_DIR) && $(JAR) cf $(JAR_FILE) . | ||
| cd $(CLASSES_DIR) && $(JAVA_ENV) $(JAR) cf $(JAR_FILE) . |
There was a problem hiding this comment.
There are more instances of this pattern where $(JAVA_ENV) could be used. Can you apply it uniformly?
hanno-becker
left a comment
hanno-becker
left a comment
There was a problem hiding this comment.
Two small issues, and could you also squash the commits? Thanks!
This sources the correct environment variables for the build process in the makefile from isabelle itself.
| $(ISABELLE) scala \ | ||
| $(JAVA_ENV) $(SCALA) \ | ||
| -classpath "$(CLASSES_DIR):$(TEST_CLASSES_DIR)" \ | ||
| IQNormalizationTest |
There was a problem hiding this comment.
This breaks the test -- the isabelle invocation must remain
2 participants
Dear all,
I am building I/Q on Linux and found that the makefile assumes macos specific paths.
This commit sources the correct environment variables for the build process in the makefile from isabelle itself, making the makefile portable between macos and linux.
Description of changes:
Environment variables like JEDIT_DIR or JEDIT_JAR are documented in isabelle getenv itself and can be sourced from there. This commit changes the makefile to do so and, as a result, makes the makefile portable between linux and macos.
I have used AI to make these changes but I confirm that it works on my linux machine. This is the current output of the debug recipe. As you can see it sources correctly paths such as JAVA_HOME from
isabelle getenv -b JAVA_HOMEBy submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.