Email Gateway (Aug 22 2022 at 17:50): Email Gateway (Aug 22 2022 at 17:50):From: Alexander Krauss <krauss@in.tum.de>
Dear list,
I have loaded the theory dependency graph of the Isabelle distribution,
the AFP and IsaFoR into structure101
(https://structure101.com/products/studio/), a comercial architecture
analysis tool that I sometimes use at work on software projects. I just
wanted to see what insights can be gained by applying this to formal
theories.
One such insight is the following: There is the convention of not
importing theories that are included in "Main", but instead using Main
itself, which avoids various technical bootstrapping issues.
I can now report that there are 52 violations of this rule. Here is a
list of them, extracted from Isabelle-2018-RC1 and the current snapshots
of AFP and IsaFoR. One might consider correcting them, just to avoid
anomalies:
AFP/Berlekamp_Zassenhaus/Arithmetic_Record_Based.thy ---> Fields.thy
AFP/CISC-Kernel/trace/Rushby-with-Control/K.thy ---> Set.thy
AFP/CISC-Kernel/trace/Rushby-with-Control/K.thy ---> List.thy
AFP/CISC-Kernel/trace/Rushby-with-Control/K.thy ---> Transitive_Closure.thy
AFP/CISC-Kernel/trace/Rushby-with-Control/List_Theorems.thy ---> List.thy
AFP/CISC-Kernel/trace/Rushby-with-Control/Option_Binders.thy --->
Option.thy
AFP/Call_Arity/Arity.thy ---> Lifting.thy
AFP/Collections/GenCF/Impl/Impl_List_Map.thy ---> List.thy
AFP/Consensus_Refined/Same_Vote.thy ---> Map.thy
AFP/Consensus_Refined/Voting.thy ---> Map.thy
AFP/DPT-SAT-Solver/DPT_SAT_Solver.thy ---> SAT.thy
AFP/Deep_Learning/Tensor_Plus.thy ---> Option.thy
AFP/Encodability_Process_Calculi/Relations.thy ---> Order_Relation.thy
AFP/Formal_SSA/SSA_CFG.thy ---> Relation.thy
AFP/Group-Ring-Module/Algebra4.thy ---> Zorn.thy
AFP/InfPathElimination/Conf.thy ---> Finite_Set.thy
AFP/InfPathElimination/SymExec.thy ---> Finite_Set.thy
AFP/Iptables_Semantics/Primitive_Matchers/Ports.thy ---> String.thy
AFP/Jordan_Hoelder/GroupIsoClasses.thy ---> List.thy
AFP/Jordan_Hoelder/GroupIsoClasses.thy ---> Groups.thy
AFP/KBPs/Extra.thy ---> Equiv_Relations.thy
AFP/Koenigsberg_Friendship/KoenigsbergBridge.thy ---> Enum.thy
AFP/Koenigsberg_Friendship/KoenigsbergBridge.thy ---> Map.thy
AFP/Network_Security_Policy_Verification/TopoS_Library.thy ---> String.thy
AFP/Nominal2/Nominal2_Abs.thy ---> Quotient.thy
AFP/Orbit_Stabiliser/Orbit_Stabiliser.thy ---> Fun.thy
AFP/Partial_Order_Reduction/Extensions/Relation_Extensions.thy --->
Wellfounded.thy
AFP/Polynomial_Interpolation/Improved_Code_Equations.thy --->
Code_Numeral.thy
AFP/Polynomial_Interpolation/Missing_Polynomial.thy ---> Set_Interval.thy
AFP/PropResPI/Prime_Implicates.thy ---> Finite_Set.thy
AFP/PropResPI/Propositional_Resolution.thy ---> Finite_Set.thy
AFP/Random_Graph_Subgraph_Threshold/Ugraph_Lemmas.thy ---> Lattices_Big.thy
AFP/Simple_Firewall/Primitives/Iface.thy ---> String.thy
AFP/Vickrey_Clarke_Groves/RelationProperties.thy --->
Conditionally_Complete_Lattices.thy
AFP/pGCL/Induction.thy ---> Conditionally_Complete_Lattices.thy
IsaFoR/Orderings/Ordered_Algebra.thy ---> Lattices.thy
IsaFoR/Orderings/Quasi_Order.thy ---> Complete_Lattices.thy
IsaFoR/Simplex/Simplex.thy ---> Order_Relation.thy
Isabelle/HOL/Cardinals/Cardinal_Arithmetic.thy --->
BNF_Cardinal_Arithmetic.thy
Isabelle/HOL/Cardinals/Cardinal_Order_Relation.thy --->
BNF_Cardinal_Order_Relation.thy
Isabelle/HOL/Cardinals/Wellorder_Constructions.thy --->
BNF_Wellorder_Constructions.thy
Isabelle/HOL/Cardinals/Wellorder_Embedding.thy --->
BNF_Wellorder_Embedding.thy
Isabelle/HOL/Cardinals/Wellorder_Relation.thy --->
BNF_Wellorder_Relation.thy
Isabelle/HOL/Computational_Algebra/Primes.thy ---> Binomial.thy
Isabelle/HOL/Library/Lattice_Syntax.thy ---> Complete_Lattices.thy
Isabelle/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy ---> HOL.thy
Isabelle/HOL/Prolog/HOHH.thy ---> HOL.thy
Isabelle/HOL/Quotient_Examples/Quotient_Int.thy ---> Nat.thy
Isabelle/HOL/ex/Computations.thy ---> Code_Numeral.thy
Isabelle/HOL/ex/Computations.thy ---> Nat.thy
Isabelle/HOL/ex/Computations.thy ---> Fun_Def.thy
Isabelle/HOL/ex/Computations.thy ---> Num.thy
Alex
Email Gateway (Aug 22 2022 at 17:50):From: Lars Hupel <hupel@in.tum.de>
Hi Alex,
this is some cool analysis.
Given that there are already a lot of these "linting" rules – mainly
concerning the ROOT files – in the AFP, I'm tempted to add such a check
there as well.
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:51):From: Lars Hupel <hupel@in.tum.de>
The following is the result of about an hour of hacking:
<https://github.com/larsrh/isabelle-lint>
Instructions are in the README. When run on the distribution ("isabelle
lint -a"), it produces a similar result as Alex's:
Found dubious imports:
HOL-Library.Lattice_Syntax -> HOL.Complete_Lattices
HOL-Matrix_LP.Compute_Oracle -> HOL.HOL
HOL-Library.Countable -> HOL.Rat
HOL-Computational_Algebra.Primes -> HOL.Binomial
HOL-Nitpick_Examples.Manual_Nits -> HOL.Real
HOL-Cardinals.Cardinal_Arithmetic -> HOL.BNF_Cardinal_Arithmetic
HOL-Cardinals.Cardinal_Order_Relation -> HOL.BNF_Cardinal_Order_Relation
HOL-Cardinals.Wellorder_Constructions -> HOL.BNF_Wellorder_Constructions
HOL-Cardinals.Wellorder_Embedding -> HOL.BNF_Wellorder_Embedding
HOL-Cardinals.Wellorder_Relation -> HOL.BNF_Wellorder_Relation
HOL-ex.Computations -> HOL.Code_Numeral
HOL-ex.Computations -> HOL.Fun_Def
HOL-ex.Computations -> HOL.Nat
HOL-ex.Computations -> HOL.Num
HOL-Quotient_Examples.Quotient_Rat -> HOL.Archimedean_Field
HOL-Quotient_Examples.Quotient_Int -> HOL.Nat
HOL-Prolog.HOHH -> HOL.HOL
Curiously, that list appears to contain more members than what
structure101 produced.
Email Gateway (Aug 22 2022 at 17:51):From: Makarius <makarius@sketis.net>
Note that there is already an administrative tool "isabelle
check_sources" -- it is not active in the normal Isabelle distribution,
only repository versions.
It would be great if the AFP checks would somehow include that, then I
would have to do fewer things manually.
Checks of theory imports have so far not been part of it, because only
Isabelle2018 has become sufficiently strict to allow this.
Makarius
Email Gateway (Aug 22 2022 at 17:51):From: Lars Hupel <hupel@in.tum.de>
Note that there is already an administrative tool "isabelle
check_sources" -- it is not active in the normal Isabelle distribution,
only repository versions.
I somehow forgot that this exists. However, it does not work if not
invoked on a Mercurial repository.
It would be great if the AFP checks would somehow include that, then I
would have to do fewer things manually.
Good point. I saw that a lot of AFP entries have an violations there.
Luckily, they can be fixed with a simple "sed". (I'll do that.)
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:51):From: Makarius <makarius@sketis.net>
I usually work with "perl -pi -e ..." because that is more portable than
"sed" -- just a habit of cross-platform shell scripting.
Traditionally, I have applied "isabelle check_sources" in a relative
lenient manner, e.g. it is often difficult to say what the private
meaning of a hard TAB in the source really is -- it requires
investigation of repository history and private mail threads to work
that out.
If these checks become more routine, we may tighten them eventually.
I propose to include your imports check soon. Is it relevant for the
Isabelle2018 release?
Makarius
Email Gateway (Aug 22 2022 at 17:51):From: Tobias Nipkow <nipkow@in.tum.de>
Using the tool by Lars I removed most such "dubious imports" in the AFP.
However, this has one drawback: in many cases I replaced an import of Rat or
Real by Complex_Main. This is a loss of information.
Note for the future: I believe there is an agreement that Complex_Main is too
large and Complex should go somewhere else. When that happens, please check all
imports and see if Complex_Main is really needed or Real_Main (or whatever it
will be called) suffices.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 17:51):From: Lars Hupel <hupel@in.tum.de>
I propose to include your imports check soon. Is it relevant for the
Isabelle2018 release?
I don't think so. It's fine to do that afterwards.
Email Gateway (Aug 22 2022 at 17:52):From: Lars Hupel <hupel@in.tum.de>
OK, I'll hold back on that then.
Email Gateway (Aug 22 2022 at 17:52):From: Makarius <makarius@sketis.net>
HOL.Rat, HOL.Real, HOL.Complex (instead of Complex_Main) sound
sufficiently prominent as further entry points, but I am not an expert
on the structure of these libraries.
One could also formalize this explicitly, and have something like
"private theory Nat" to say that HOL.Nat should be only accessible
within its own session.
In any case it is something to be reconsidered after the release.
Makarius
Email Gateway (Aug 22 2022 at 17:52):From: Tobias Nipkow <nipkow@in.tum.de>
On 18/07/2018 19:20, Makarius wrote:
On 18/07/18 17:08, Tobias Nipkow wrote:
Using the tool by Lars I removed most such "dubious imports" in the AFP.
However, this has one drawback: in many cases I replaced an import of
Rat or Real by Complex_Main. This is a loss of information.Note for the future: I believe there is an agreement that Complex_Main
is too large and Complex should go somewhere else. When that happens,
please check all imports and see if Complex_Main is really needed or
Real_Main (or whatever it will be called) suffices.HOL.Rat, HOL.Real, HOL.Complex (instead of Complex_Main) sound
sufficiently prominent as further entry points, but I am not an expert
on the structure of these libraries.
In the light of that comment and the fact that nobody voiced dissent, I will
probably go back to the more specific imports in the AFP.
Tobias
One could also formalize this explicitly, and have something like
"private theory Nat" to say that HOL.Nat should be only accessible
within its own session.In any case it is something to be reconsidered after the release.
Makarius
Email Gateway (Aug 22 2022 at 18:14):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Just for the record: some imports in the distribution have been
canonized in 4ce18f389f53.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 18:14):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Something like that came also to my mind, but it is challenging to come
up with reasonable default rules – you do not want to lock up
specifications by default as you would do with implementations.
Florian
signature.asc
Last updated: Apr 25 2024 at 12:23 UTC