From: Jakub Kądziołka <firstname.lastname@example.org>
Dear Isabelle users,
inside of jEdit, I can Ctrl+click to view the definition of anything I
use in my theory. Sometimes, this will take me to a file inside
~~/src/HOL, and in those files, this mechanism doesn't work anymore.
I suspect this has something to do with the error at the top of the
Cannot update finished theory "HOL.Rings"
Is this a misconfiguration on my part, or is it an unavoidable bug?
Currently, I can cope by temporarily including the constant or type I'm
interested in the theory I'm working on, but it's cumbersome and can
easily break if a name is defined in multiple places.
I suppose another workaround would be to start jedit with the -l Pure
option, so that HOL gets reprocessed on startup instead of loading a
heap image. In my case, this is unworkable, as I'm actually interested
in following around the definitions in HOL-Analysis and HOL-Algebra,
which I include in a custom session to avoid re-checking these heavy
sessions every time I load them.
I would be interested in any other workarounds or fixes.
From: Makarius <email@example.com>
You can also try https://search.isabelle.in.tum.de --- it is still somewhat
experimental, but already quite usable.
Your observation is correct that already loaded (or "finished") theories don't
get Prover IDE markup and thus no hyperlinks. This is neither a "bug" nor a
"feature": it is merely a limitation of the present approach (since approx.
2011). Many other high-end IDEs have similar limitation, but also add-on
mechanisms to overcome it (e.g. IntelliJ IDEA disassembles library jar modules
on the spot).
One happy day, the Isabelle Prover IDE will be able to do something similar,
but it takes time to get there, and one must avoid applying too much force in
"fixes" that are apt to devastate a delicate eco-system.
Last updated: Jan 25 2022 at 01:11 UTC