[isabelle-dev] bad session structure

Lawrence Paulson lp15 at cam.ac.uk
Wed May 9 13:25:56 CEST 2018


I'm getting this message again. What gives? Everything is fully updated.

~/isabelle/Repos/src/HOL: hg id
2e5b737810a6 tip

Larry

Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Category3.Limit" via "Category3.FreeCategory" via "Category3.Category") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Category3/Category.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Category3" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Category3/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Category2.MonadicEquationalTheory" via "Category2.Category") (line 8 of "/Users/lp15/isabelle/afp/devel/thys/Category2/Category.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Category2" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Category2/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Topology.LList_Topology" via "Topology.Topology") (line 10 of "/Users/lp15/isabelle/afp/devel/thys/Topology/Topology.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Topology" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Topology/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Category.Cat") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Category/Cat.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Category" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Category/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Card_Partitions.Card_Partitions" via "Card_Partitions.Set_Partition") (line 8 of "/Users/lp15/isabelle/afp/devel/thys/Card_Partitions/Set_Partition.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Bell_Numbers_Spivey" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Bell_Numbers_Spivey/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Graph_Theory.Graph_Theory" via "Graph_Theory.Subdivision" via "Graph_Theory.Funpow") (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Graph_Theory/Funpow.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Graph_Theory" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Graph_Theory/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Card_Partitions.Card_Partitions" via "Card_Partitions.Set_Partition") (line 8 of "/Users/lp15/isabelle/afp/devel/thys/Card_Partitions/Set_Partition.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Card_Partitions" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Card_Partitions/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "VectorSpace.FunctionLemmas") (line 6 of "/Users/lp15/isabelle/afp/devel/thys/VectorSpace/FunctionLemmas.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Deep_Learning_Lib" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Deep_Learning/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "ArrowImpossibilityGS.GS" via "ArrowImpossibilityGS.Arrow_Order") (line 5 of "/Users/lp15/isabelle/afp/devel/thys/ArrowImpossibilityGS/Thys/Arrow_Order.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "ArrowImpossibilityGS" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/ArrowImpossibilityGS/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "VectorSpace.VectorSpace" via "VectorSpace.MonoidSums" via "VectorSpace.FunctionLemmas") (line 6 of "/Users/lp15/isabelle/afp/devel/thys/VectorSpace/FunctionLemmas.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "VectorSpace" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/VectorSpace/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "LinearQuantifierElim.QEdlo" via "LinearQuantifierElim.DLO" via "LinearQuantifierElim.QE" via "LinearQuantifierElim.Logic") (line 6 of "/Users/lp15/isabelle/afp/devel/thys/LinearQuantifierElim/Thys/Logic.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "LinearQuantifierElim" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/LinearQuantifierElim/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "VectorSpace.VectorSpace" via "VectorSpace.MonoidSums" via "VectorSpace.FunctionLemmas") (line 6 of "/Users/lp15/isabelle/afp/devel/thys/VectorSpace/FunctionLemmas.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "JNF-AFP-Lib" (line 38 of "/Users/lp15/isabelle/afp/devel/thys/Polynomial_Factorization/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Planarity_Certificates.Planarity_Certificates" via "Planarity_Certificates.Kuratowski_Combinatorial" via "Planarity_Certificates.Planar_Complete" via "Planarity_Certificates.Digraph_Map_Impl" via "Planarity_Certificates.Graph_Genus" via "Graph_Theory.Graph_Theory" via "Graph_Theory.Subdivision" via "Graph_Theory.Funpow") (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Graph_Theory/Funpow.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Planarity_Certificates" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Planarity_Certificates/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Dirichlet_Series.Arithmetic_Summatory_Asymptotics" via "Dirichlet_Series.Arithmetic_Summatory" via "Dirichlet_Series.More_Totient" via "Dirichlet_Series.Moebius_Mu" via "Dirichlet_Series.Dirichlet_Series") (line 13 of "/Users/lp15/isabelle/afp/devel/thys/Dirichlet_Series/Dirichlet_Series.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Dirichlet_Series" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Dirichlet_Series/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Group-Ring-Module.Algebra9" via "Group-Ring-Module.Algebra8" via "Group-Ring-Module.Algebra7" via "Group-Ring-Module.Algebra6" via "Group-Ring-Module.Algebra5" via "Group-Ring-Module.Algebra4" via "Group-Ring-Module.Algebra3" via "Group-Ring-Module.Algebra2" via "Group-Ring-Module.Algebra1") (line 27 of "/Users/lp15/isabelle/afp/devel/thys/Group-Ring-Module/Algebra1.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Group-Ring-Module" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Group-Ring-Module/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness" via "Jordan_Normal_Form.Matrix_Kernel" via "Jordan_Normal_Form.VS_Connect" via "VectorSpace.VectorSpace" via "VectorSpace.MonoidSums" via "VectorSpace.FunctionLemmas") (line 6 of "/Users/lp15/isabelle/afp/devel/thys/VectorSpace/FunctionLemmas.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Stochastic_Matrices" (line 2 of "/Users/lp15/isabelle/afp/devel/thys/Stochastic_Matrices/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Twelvefold_Way.Twelvefold_Way" via "Twelvefold_Way.Preliminaries") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Twelvefold_Way/Preliminaries.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Twelvefold_Way" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Twelvefold_Way/ROOT")


More information about the isabelle-dev mailing list