Email Gateway (Jan 03 2021 at 23:58): Email Gateway (Jan 03 2021 at 23:58):From: Jakub Kądziołka <kuba@kadziolka.net>
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
theory file:
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.
Kind regards,
Jakub Kądziołka
Email Gateway (Jan 04 2021 at 12:37):From: Makarius <makarius@sketis.net>
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.
Makarius
Last updated: Jul 15 2022 at 23:21 UTC