Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Malformed theory files in Isabelle/src

view this post on Zulip Email Gateway (Apr 18 2024 at 02:58):

From: Xiaokun Luan <luanxiaokun@pku.edu.cn>
Hi all,

I found that many theory files located in Isabelle/src seem to exhibit issues
when loaded in jEdit.
However, most of these files can be imported with no error and can be built
successfully.
I'm wondering why a theory file that cannot pass proof checking in jEdit can
be built and imported with no error.
Is this as expected and intentional, or am I doing something wrong?

Here are some examples:

  1. Theories that are not listed in the ROOT files but can be imported

I found four files of this kind:

Partial.thy is importing "Tutorial.While_Combinator", which has been moved to
HOL-Library, so it cannot be imported.
WFrec.thy uses deprecated command recdef, QuoRem.thy complains that there is
illegal free variable.
Hotel_Example_Small_Generator.thy complains there is a type error.
All of these three files can be imported with no error.

  1. Theories that are not listed in the ROOT files and cannot be imported

Theory files in Doc/Tutorial/Recdef seem to be about the deprecated command
recdef.
They cannot be imported since the folder Recdef is not declared in the
Tutorial session.
The first two kinds of malformed files are not checked during the build
process.

  1. Theories that are listed in the ROOT files but have errors

I found seven theory files listed in the ROOT files that throw errors when
loaded in jEdit:

All of these files can be imported with no error, and the build process also
succeeds.
I'm aware that some theory files use oops to skip unsuccessful proof attempts,
but none of these files do that.

Maybe the first two kinds of malformed (if so) theory files could just be
removed to keep things a little tidier.
As for the third kind of files, I'm not sure if these errors are expected,
since they can be built and imported, or if they are just malformed and should
be fixed or removed.

Cheers,
Xiaokun

view this post on Zulip Email Gateway (Apr 18 2024 at 08:32):

From: Fabian Huch <huch@in.tum.de>
The recdef doc looks like it might actually be unused (nowadays there is
only old_recdef), maybe someone knows what should happen with the docs.

As for your other problems, you have some misconceptions here:

(1) Theory files do not all need to be listed in a ROOT file -- for
instance, they can just be imported by a theory that is listed (e.g.,
QuotRem is imported by Greatest_Common_Divisor).

(3) You'll have to start jEdit with the right logic/session -- use
isabelle jedit -R HOL-Proofs-Extraction, for example.

Fabian

view this post on Zulip Email Gateway (Apr 22 2024 at 02:58):

From: Xiaokun Luan <luanxiaokun@pku.edu.cn>
Hi Fabian,

Thanks for your reply and explanation, it seems clearer to me now.

Theory files do not all need to be listed in a ROOT file, but I've seen many
cases (mainly in AFP) where the theory file is neither imported by any other
theory files in the session, nor listed in the ROOT file. I think in such
case, this file will never be checked during the build process, correct?

What makes it worse is that, if the file (that not listed nor imported) is
placed in the root folder of the session, or in any directory that is listed
in the ROOT file, it can still be imported by using A.B where A is the session
name and B the theory name. (Please correct me if I'm wrong) I imagine that
these files will eventually end up like the malformed doc theory files. Though
things still work as long as we don't import these "dead code", I think it
would be tidier if these files can be listed in the ROOT file and fixed
accordingly, or just removed.

view this post on Zulip Email Gateway (Apr 22 2024 at 12:23):

From: Fabian Huch <huch@in.tum.de>
On 4/22/24 04:58, Xiaokun Luan wrote:

Theory files do not all need to be listed in a ROOT file, but I've seen many
cases (mainly in AFP) where the theory file is neither imported by any other
theory files in the session, nor listed in the ROOT file. I think in such
case, this file will never be checked during the build process, correct?

Yes. In fact, you can find out those particular theories using (with
isabelle-devel + afp-devel installed):

isabelle afp_check_roots -C unused_thys

What makes it worse is that, if the file (that not listed nor imported) is
placed in the root folder of the session, or in any directory that is listed
in the ROOT file, it can still be imported by using A.B where A is the session
name and B the theory name. (Please correct me if I'm wrong)
Unfortunately yes.
I imagine that
these files will eventually end up like the malformed doc theory files. Though
things still work as long as we don't import these "dead code", I think it
would be tidier if these files can be listed in the ROOT file and fixed
accordingly, or just removed.

Agreed. For new submissions, we do not allow such dangling theories but
yes there are some entries that still have them -- it is on the authors
to check their material if it is relevant and should be checked or
irrelevant and can be removed. I guess one could message them about that.

Fabian

Last updated: May 05 2024 at 01:11 UTC