Re: [isabelle] Verbose output for isatool make



On Tue, 30 Jun 2009, Matthew Wampler-Doty wrote:

isatool usedir -b -g true ~/isabelle/heaps/Isabelle2007/polyml-5.1_ppc-darwin/Compute ProcessGraphs

which outputs:

### Legacy feature: loading attached ML script "MatrixIneq.ML"
*** 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

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.