Stream: Beginner Questions

Topic: Isabelle build fails with "malformed command syntax"

Chengsong Tan (May 07 2024 at 16:34):

Hi,

I was trying to build an Isabelle session.
I have changed into the directory where all my theory files I need to work with reside in.
I have my theory file, called NewSARspSFwdM.thy and the ROOT file:

session "My_Session" = HOL +
  theories
    NewSARspSFwdM

NewSARspSFwdM is the top-level file, and imports the other files, so I did not include other theories that are being imported.
The error was like this:

isabelle build -D .
Running My_Session ...
My_Session FAILED (see also "isabelle build_log -H Error My_Session")
*** Failed to load theory "My_Session.CoherenceProperties" (unresolved "My_Session.Transposed")
*** Failed to load theory "My_Session.BuggyRules" (unresolved "My_Session.CoherenceProperties")
*** Failed to load theory "My_Session.BasicInvariants" (unresolved "My_Session.BuggyRules")
*** Failed to load theory "My_Session.NewSARspSFwdM" (unresolved "My_Session.BasicInvariants")
*** Malformed command syntax
*** At command "<malformed>" (line 1 of "~/Dropbox/cxl2/cxl-formalisation/Transposed.thy")
Unfinished session(s): My_Session
0:00:05 elapsed time

But when checking with jedit, the Transposed.thy file gives no problems. What could be the issue?

NewSARspSFwdM.thy
BasicInvariants.thy
BuggyRules.thy
CoherenceProperties.thy
Transposed.thy
ROOT

Mathias Fleury (May 07 2024 at 16:42):

Besides the fact that the file has no end, '‹' is not a character you can use. In Isabelle/jedit, File > Reload as > UTF8-Isabelle.

Chengsong Tan (May 07 2024 at 16:48):

Mathias Fleury said:

Besides the fact that the file has no end, '‹' is not a character you can use. In Isabelle/jedit, File > Reload as > UTF8-Isabelle.

I must have copy-pasted from somewhere this symbol.....what a stupid mistake

Chengsong Tan (May 07 2024 at 16:48):

Do ROOT files have to end with an end? Otherwise I can't find any other files listed without the end keyword.

Mathias Fleury (May 07 2024 at 16:49):

No the theory file has no end

Mathias Fleury (May 07 2024 at 16:49):

theory Transposed imports Main
begin
―‹
...
›

Mathias Fleury (May 07 2024 at 16:49):

ah sorry my bad

Mathias Fleury (May 07 2024 at 16:50):

the line breaks where exactly where my terminal ended, so it did not realize that the file was longer than that

Mathias Fleury (May 07 2024 at 16:51):

BTW you have also ∄, ⇒ as invalid characters

Mathias Fleury (May 07 2024 at 16:51):

⦈, Σ, ...

Last updated: Dec 21 2024 at 16:20 UTC