Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] use_thy "Pure";

Email Gateway (Aug 18 2022 at 09:58):

From: Priya Gopalan <priya.g@ed.ac.uk>
In an attempt to build the raw Isabelle process,
I am trying to get my ML system to make sense of this file:
src/Pure/ROOT.ML
It goes fine till the point when its given

use_thy "Pure";

upon when it complains with the following.

Loading theory "Pure
*** Uninitialized theory data "Isar/attributes"

I have made some changes to the source inorder to suit the dialect of
ML that I am using (alice). I have been trying to investigate if this
error is because of

(1)-any of the changes that i have made
(2)-of the implementation features of alice

I can say that (2) is not the case, as i have tried the same experiment
(with the same source) in the SML-NJ system and i get the same error.

I am wondering if any of you have ever done something like this before
and if you can help.

I will be very grateful for any info on the sequence of function calls
involved in "use_thy" and the dependecies.

Thanks in advance for your help,

Priya

Email Gateway (Aug 18 2022 at 09:59):

From: Makarius <makarius@sketis.net>
On Tue, 12 Dec 2006, Priya Gopalan wrote:

I have made some changes to the source inorder to suit the dialect of ML
that I am using (alice). I have been trying to investigate if this error
is because of

(1)-any of the changes that i have made
(2)-of the implementation features of alice

I can say that (2) is not the case, as i have tried the same experiment
(with the same source) in the SML-NJ system and i get the same error.

Maybe you can show your changes to the sources in order to get an idea
what is going on here.

I will be very grateful for any info on the sequence of function calls
involved in "use_thy" and the dependecies.

The final use_thy "Pure" of the Isabelle bootstrap depends on almost
everything defined before.

Makarius

Last updated: May 03 2024 at 08:18 UTC