[isabelle-dev] unbound Code.add_type_cmd

[Lukas Bulwahn]

Changesets f523923d8182 and 3bc39cfe27fe should have resolved the issue.

Lukas

On 09/02/2011 11:40 AM, Lukas Bulwahn wrote:
> The reason that this issue has just recently become apparent, is due 
> to changes 322d1657c40c ff. by Andreas Lochbihler. He assisted in 
> replacing (Stefan Berghofer's) SML code generator invocations by 
> generic code generator invocations to enable the long-term removal of 
> the SML code generator.
>
> I agree, Florian knows probably best how to resolve this issue easy 
> and clean.
>
> In the long run, we are planning to get rid of Executable_Set and 
> add_type_cmd anyway by providing data refinement within the logic 
> (and/or the current efforts towards a own set type).
>
> Lukas
>
>
> On 08/29/2011 04:37 PM, Makarius wrote:
>> For quite some time isatest produces the following error with SML/NJ:
>>
>> Loading theory "Executable_Set"
>> *** Error in 
>> /mnt/home/isatest/isadist/Isabelle_29-Aug-2011/src/HOL/Library/Executable_Set.thy
>> *** <instream>:2.3-2.20 Error: unbound variable or constructor: 
>> add_type_cmd in path Code.add_type_cmd
>> *** At command "setup" (line 25 of 
>> "/mnt/home/isatest/isadist/Isabelle_29-Aug-2011/src/HOL/Library/E
>>
>> This is because SML/NJ does not have managed ML names spaces within 
>> the theory context as Poly/ML.  So any overriding of structure Code 
>> on the toplevel stays persistent.  The conflict is caused by the code 
>> generator itself: it provides a static structure Code (in 
>> ~~/src/Pure/Isar/code.ML), and uses the same name to wrap up 
>> generated code in certain situations. Grepping for "Code" in the 
>> sources reveals some such places.
>>
>> Florian probably knows best how to avoid this overlap.
>>
>>
>>     Makarius
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>