[isabelle-dev] CVS

[Makarius]

On Tue, 25 Mar 2008, Amine Chaieb wrote:

> Pure FAILED
> (see also /Users/chaieb/isabelle/heaps//polyml-5.2_ppc-darwin/log/Pure)
> 
> {getChar = get, putString = put, lineNumber = fn ... => ..., fileName = 
> name,
>    nameSpace = ...}
> 
> Error: in 'ML-Systems/polyml.ML', line 39.
> Can't unify (unit -> string) * (string -> unit) with
>     {getChar: unit -> String.char option, fileName: 'a, nameSpace: bad,
>       putString: string -> unit, lineNumber: ...} (Field 1 missing) 
> Found near
>     while not(List.null(!(in_buffer))) do
>     PolyML.compiler({getChar = get, putString = ..., ...})(())

Version 5.2 looks like the CVS snapshot of Poly/ML, which changes 
frequently, so you need to update that as well.


> When I use my Older PolyML installation (5.0), Compiling Pure terminates 
> in 0 sec without an error message. The log file though contain the 
> following:

>     PolyML.SaveState.saveState(
>     "/Users/chaieb/isabelle/heaps//polyml-5.1_ppc-darwin/Pure");
>     true
>     )

This looks like the version 5.0 has been declared as 5.1, which just does 
not work.


As usual, it is most convenient to use the contributed systems (Poly/ML, 
ProofGeneral) from the Isabelle download site.  Here the official Poly/ML 
5.1 is already prepackaged for various platforms, including ppc-darwin.


	Makarius