Email Gateway (Aug 18 2022 at 13:40): Email Gateway (Aug 18 2022 at 13:40):From: Matthew Wampler-Doty <negacthulhu@gmail.com>
Hi,
I'm getting a compile error in a command "isatool make" that I am
issuing, and I am would like to get more verbose output so I can
diagnose the problem.
Thank you in advance!
~Matthew P. Wampler-Doty
Email Gateway (Aug 18 2022 at 13:40):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Matthew,
I must confess I do not understand your problem in full without more
context.
It seems that you are using an Isabelle version previous to the current
2009 release, because since then "isatool" has been replaced by "isabelle".
Note that "isatool/isabelle" make is just a wrapper around GNU make,
which provides an enriched environment and defaults to "IsaMakefile"
instead of "Makefile" as makefile.
So if a problem occurs in your makefile, you may use the debugging
facilities GNU make provides ("make --help" should gie you some hints).
Otherwise, a typical session will produce a logfile which you can
inspect -- in case of an error, a hint where to find the log will be
printed.
If these hints are not helpful, please provide the shell command and the
the shell output for a closer diagnosis.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 13:41):From: Matthew Wampler-Doty <negacthulhu@gmail.com>
Florian Haftmann wrote:
Hi Matthew,
I'm getting a compile error in a command "isatool make" that I am
issuing, and I am would like to get more verbose output so I can
diagnose the problem.
I must confess I do not understand your problem in full without more
context.Thank you Florian.
Specifically, I'm working with Isabelle2007... I am working with code
that has not been ported to Isabelle 2009
Anyway, working through the makefile, the line that my compile is
failing on is:
isatool usedir -b -g true
~/isabelle/heaps/Isabelle2007/polyml-5.1_ppc-darwin/Compute ProcessGraphs
which outputs:
<code>
Building ProcessGraphs ...
ProcessGraphs FAILED
(see also
~/isabelle/heaps/Isabelle2007/polyml-5.1_ppc-darwin/log/ProcessGraphs)
*** fun ...(...) = case ... of ...
*** datatype bound_type = UPPER | ...
*** fun ...
*** structure BoundsTab = TableFun(struct ... ... end)
*** ...
*** ...
*** end
*** At command "use".
*** Exception- TOPLEVEL_ERROR raised
make: ***
[~/isabelle/heaps/Isabelle2007/polyml-5.1_ppc-darwin/ProcessGraphs] Error 1
</code>
This is perhaps not so illuminating. Looking at the log file mentioned
in the error output I see:
*** Error: in '~/flyspeck/obua_flyspeckII.distribute/process
graphs/MatrixIneq.ML', line 18.
*** Structure (SparseMatrix) has not been declared
*** Found near val get_vars : matrixineq -> cterm SparseMatrix.vector
It looks like this file is being called in the following "uses" call:
uses "decimals.ML" "Script.ML" "Darts.ML" "GraphUtil.ML"
"GraphLogic.ML" "sp
arsematrix.ML" "matrixineq.ML" "finallp.ML" "process_graphs.ML"
and it should be that sparsematrix.ML, which defines
SparseMatrix.vector, should be loaded by the time MatrixIneq.ML gets
called...
Thank you Florian for your help!
~Matt
It seems that you are using an Isabelle version previous to the current
2009 release, because since then "isatool" has been replaced by "isabelle".Note that "isatool/isabelle" make is just a wrapper around GNU make,
which provides an enriched environment and defaults to "IsaMakefile"
instead of "Makefile" as makefile.So if a problem occurs in your makefile, you may use the debugging
facilities GNU make provides ("make --help" should gie you some hints).Otherwise, a typical session will produce a logfile which you can
inspect -- in case of an error, a hint where to find the log will be
printed.If these hints are not helpful, please provide the shell command and the
the shell output for a closer diagnosis.Hope this helps,
Florian
Email Gateway (Aug 18 2022 at 13:45):From: Makarius <makarius@sketis.net>
The "legacy feature" warning indicates either a very old-stylish use of ML
files by Steven Obua, or the usual pitfall of the case-insensible
file-system of Mac OS. There is probably a file called matrixineq.ML
which gets loaded earlier than anticipated.
Where can I get the obua_flyspeckII.distribute sources?
Makarius
Last updated: May 03 2024 at 08:18 UTC