Email Gateway (Aug 18 2022 at 17:34): Email Gateway (Aug 18 2022 at 17:34):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi all,
I noticed that
isabelle make
will always execute an existing IsaMakefile, even for
isabelle make -f other-makefile
is there a specific reason for this behavior (which I did not expect)?
cheers
chris
Email Gateway (Aug 18 2022 at 17:34):From: Makarius <makarius@sketis.net>
This depends on make alone, whichever version is used here. The isabelle
wrapper merely invokes "make -f IsaMakefile" within the standard settings
environment. The idea is to use that make file as default. In Unix
command line tools repeated options either accumulate, or have a tendency
to prefer the last occurrence, although this is not fully standardized.
So the meaning of some extra -f is hard to predict.
Since the basic principle behind isabelle make is to do nothing specific,
apart from providing some reasonable defaults, you can always invoke
completely different make command lines like that:
isabelle env make -f other-makefile
Makarius
Last updated: Apr 19 2024 at 20:15 UTC