[isabelle-dev] Options to pass to "isabelle jedit" after session directory reform

Jasmin Blanchette j.c.blanchette at vu.nl
Thu Sep 26 15:20:15 CEST 2019


Hi all,

I have updated the Isabelle and AFP development repositories and cannot figure how to do something pretty basic. I have my own theory, let's call it "Foo", in a private repository outside the AFP, and "Foo" imports "Concurrent_Revisions.Operational_Semantics" (i.e. "Operational_Semantics.thy" from the "Concurrent_Revisions" AFP entry). Back in August, when launching Isabelle/JEdit I would write

	isabelle jedit -d ~/afp/thys Foo.thy

and that worked. (I also have 'init_component "$USER_HOME/afp"' in "~/.isabelle/etc/settings".) But now (Isabelle/ffbe7784cc85 and AFP/66bfe59e1850) this has stopped working. I get a red squiggly line under the import of "Concurrent_Revisions.Operational_Semantics" in "Foo".

I studied the "isabelle jedit" options, as documented in "jedit.pdf", but couldn't figure out how to proceed. I'd be grateful for any hint.

Jasmin



More information about the isabelle-dev mailing list