Stream: Beginner Questions

Topic: nothing known about theory

Qiyuan Xu (Mar 19 2025 at 07:38):

Sorry for this disturbance. This post was a moment of foolishness on my part, please close/dismiss this thread.

This post is about some dirty hacks that users shouldn't take. Please close and ignore this post.

Hi, until today, I believe I can be called an Isabelle hacker, but I find today I cannot troubleshoot even a simple problem.

I have following package hierarchy:

auto_sledgehammer/ROOT

session Auto_Sledgehammer = HOL +
  theories Auto_Sledgehammer
  document_files
    "root.tex"

Isa_REPL/ROOT

session Isa_REPL = Auto_Sledgehammer +
  theories Isa_REPL

REPL224139/ROOT

session REPL224139 = HOL
 + sessions Auto_Sledgehammer Isa_REPL
   theories REPL224139

Isa_REPL/Isa_REPL.thy

theory Isa_REPL
  imports Auto_Sledgehammer.Auto_Sledgehammer
begin

ML_file \<open>contrib/mlmsgpack/mlmsgpack-aux.sml\<close>
ML_file \<open>contrib/mlmsgpack/realprinter-packreal.sml\<close>
ML_file \<open>contrib/mlmsgpack/mlmsgpack.sml\<close>

ML_file \<open>library/REPL.ML\<close>
ML_file \<open>library/REPL_serializer.ML\<close>
ML_file \<open>library/REPL_aux.ML\<close>
ML_file \<open>library/Server.ML\<close>

end

REPL224139/REPL224139.thy

theory REPL224139
imports "Isa_REPL.Isa_REPL"
begin
ML \<open>
REPL.disable_output () ;
Thy_Info.register_thy @{theory Isa_REPL} ;
Isabelle_Thread.join (REPL_Server.startup (Path.explode "/tmp/repl_outputs") NONE "127.0.0.1:6666")
\<close>
end

The problem is I try to build the packages above.

isabelle build Auto_Sledgehammer # OK!
isabelle build Isa_REPL # OK!
isabelle build REPL224139 # error!
# *** Theory loader: nothing known about theory "Auto_Sledgehammer.Auto_Sledgehammer"
# ***
# *** At command "ML" (line 4 of "/tmp/tmp.S6GNgYxXUy/REPL224139.thy")

The theory loader cannot find Auto_Sledgehammer.Auto_Sledgehammer but I have specify it in both REPL224139/ROOT and Isa_REPL/ROOT.

Qiyuan Xu (Mar 19 2025 at 07:41):

Alternatively, everything works if I change REPL224139/ROOT into

session REPL224139 = Auto_Sledgehammer
 + sessions Isa_REPL
   theories REPL224139

However, this change is not acceptable in my REPL system. Could some one tell me what is the exact difference between a parent session and the session indicated in the sessions clause? This subtle behavior is really confusing

Mathias Fleury (Mar 19 2025 at 07:46):

auto_sledgehammer/ROOT

is a typo for Auto_Sledgehammer right? or are you relying on the underlying file system to be case insensitive? (yes macos users, you are the only ones that can do that)

Mathias Fleury (Mar 19 2025 at 07:46):

(because this is exactly the kind of weird bugs I would expect to happen if you the get the case wrong)

Qiyuan Xu (Mar 19 2025 at 07:48):

I am a fool!
I find I should just register the Auto_Sledgehammer theory to the system.

REPL224139/REPL224139.thy

theory REPL224139
imports "Isa_REPL.Isa_REPL"
begin
ML \<open>
REPL.disable_output () ;
(*Add the following line solves the issue!*)
Thy_Info.register_thy @{theory Auto_Sledgehammer} ;
Thy_Info.register_thy @{theory Isa_REPL} ;
Isabelle_Thread.join (REPL_Server.startup (Path.explode "/tmp/repl_outputs") NONE "127.0.0.1:6666");
error "IGNORE THIS ERROR"
\<close>
end

Cry, this must be the payback for all the dirty hacks I've taken. Sorry for the disturbance, let's drop this topic/thread.

Qiyuan Xu (Mar 19 2025 at 07:56):

Mathias Fleury said:

(because this is exactly the kind of weird bugs I would expect to happen if you the get the case wrong)

Hi, Mathias, thank your response. The error in this post was caused by some dirty hacks taken by me (and my sudden foolishness). Please just ignore this post, and my bad.

Last updated: Apr 18 2025 at 20:21 UTC