Re: [isabelle-dev] Bad session structure
This is because of a name change in the distribution. The AFP has been updated some 10 minutes later but your test run still saw the old version. It should work now. Tobias On 25/06/2018 15:25, Lawrence Paulson wrote: I still get this upon start-up. Any idea why? ebdd5508f386+ tip Larry Cannot load theory "HOL-Data_Structures.Priority_Queue" The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue" (required by "Priority_Queue_Braun.Priority_Queue_Braun") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Priority_Queue_Braun/Priority_Queue_Braun.thy") No such file: "HOL-Data_Structures.Priority_Queue" The error(s) above occurred in session "Priority_Queue_Braun" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Priority_Queue_Braun/ROOT") Cannot load theory "HOL-Data_Structures.Priority_Queue" The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue" (required by "Amortized_Complexity.Skew_Heap_Analysis" via "Skew_Heap.Skew_Heap") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/Skew_Heap.thy") No such file: "HOL-Data_Structures.Priority_Queue" The error(s) above occurred in session "Amortized_Complexity" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Amortized_Complexity/ROOT") Cannot load theory "HOL-Data_Structures.Priority_Queue" The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue" (required by "Skew_Heap.Skew_Heap") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/Skew_Heap.thy") No such file: "HOL-Data_Structures.Priority_Queue" The error(s) above occurred in session "Skew_Heap" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/ROOT") Cannot load theory "HOL-Data_Structures.Priority_Queue" The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue" (required by "Pairing_Heap.Pairing_Heap_Tree") (line 8 of "/Users/lp15/isabelle/afp/devel/thys/Pairing_Heap/Pairing_Heap_Tree.thy") No such file: "HOL-Data_Structures.Priority_Queue" The error(s) above occurred in session "Pairing_Heap" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Pairing_Heap/ROOT") ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Bad session structure
I still get this upon start-up. Any idea why? ebdd5508f386+ tip Larry Cannot load theory "HOL-Data_Structures.Priority_Queue" The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue" (required by "Priority_Queue_Braun.Priority_Queue_Braun") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Priority_Queue_Braun/Priority_Queue_Braun.thy") No such file: "HOL-Data_Structures.Priority_Queue" The error(s) above occurred in session "Priority_Queue_Braun" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Priority_Queue_Braun/ROOT") Cannot load theory "HOL-Data_Structures.Priority_Queue" The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue" (required by "Amortized_Complexity.Skew_Heap_Analysis" via "Skew_Heap.Skew_Heap") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/Skew_Heap.thy") No such file: "HOL-Data_Structures.Priority_Queue" The error(s) above occurred in session "Amortized_Complexity" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Amortized_Complexity/ROOT") Cannot load theory "HOL-Data_Structures.Priority_Queue" The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue" (required by "Skew_Heap.Skew_Heap") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/Skew_Heap.thy") No such file: "HOL-Data_Structures.Priority_Queue" The error(s) above occurred in session "Skew_Heap" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/ROOT") Cannot load theory "HOL-Data_Structures.Priority_Queue" The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue" (required by "Pairing_Heap.Pairing_Heap_Tree") (line 8 of "/Users/lp15/isabelle/afp/devel/thys/Pairing_Heap/Pairing_Heap_Tree.thy") No such file: "HOL-Data_Structures.Priority_Queue" The error(s) above occurred in session "Pairing_Heap" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Pairing_Heap/ROOT") ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] bad session structure
It seems that I can fix this by updating afp-devel again. Larry > On 9 May 2018, at 12:37, Lars Hupel wrote: > > Do you have any uncommitted changes? Maybe in the AFP? > > ~/work/isabelle (default)$ isabelle-dev build -bva -D '$AFP' > > works fine for me. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] bad session structure
> I'm getting this message again. What gives? Everything is fully updated. > > ~/isabelle/Repos/src/HOL: hg id > 2e5b737810a6 tip Do you have any uncommitted changes? Maybe in the AFP? ~/work/isabelle (default)$ isabelle-dev build -bva -D '$AFP' works fine for me. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] bad session structure
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.FunctionLemma
Re: [isabelle-dev] Bad session structure: may cause problems with theory imports
Hi Larry, I guess you have to update your local AFP clone also. Hope this helps, Florian Am 25.04.2018 um 18:03 schrieb Lawrence Paulson: > In the past couple of days, upon launching Isabelle jEdit, I get an alert box > with the message above and the attached text. Any ideas? > > Larry > > ~/isabelle/Repos/src/Pure: hg id > 362baebe25a5 tip > > Cannot load theory "HOL-Library.Code_Char" > The error(s) above occurred for theory "HOL-Library.Code_Char" > (required by "Affine_Arithmetic.Affine_Arithmetic" via > "Affine_Arithmetic.Ex_Affine_Approximation" via "Affine_Arithmetic.Print") > (line 8 of "/Users/lp15/isabelle/afp/devel/thys/Affine_Arithmetic/Print.thy") > No such file: "HOL-Library.Code_Char" > The error(s) above occurred in session "HOL-ODE-Refinement" (line 19 of > "/Users/lp15/isabelle/afp/devel/thys/Ordinary_Differential_Equations/ROOT") > Cannot load theory "HOL-Library.Code_Char" > The error(s) above occurred for theory "HOL-Library.Code_Char" > (required by "JinjaThreads.Basic_Main") (line 5 of > "/Users/lp15/isabelle/afp/devel/thys/JinjaThreads/Basic/Basic_Main.thy") > No such file: "HOL-Library.Code_Char" > The error(s) above occurred in session "JinjaThreads" (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/JinjaThreads/ROOT") > Cannot load theory "HOL-Library.Code_Char" > The error(s) above occurred for theory "HOL-Library.Code_Char" > (required by "DFS_Framework.DFS_Framework" via "DFS_Framework.Param_DFS" via > "CAVA_Base.CAVA_Base" via "CAVA_Base.CAVA_Code_Target" via > "CAVA_Base.Code_String") (line 9 of > "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy") > No such file: "HOL-Library.Code_Char" > The error(s) above occurred in session "Maxflow_Lib" (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/Flow_Networks/ROOT") > Cannot load theory "HOL-Library.Code_Char" > The error(s) above occurred for theory "HOL-Library.Code_Char" (line 14 of > "/Users/lp15/isabelle/afp/devel/thys/Iptables_Semantics/ROOT") > No such file: "HOL-Library.Code_Char" > The error(s) above occurred in session "Iptables_Semantics" (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/Iptables_Semantics/ROOT") > Cannot load theory "HOL-Library.Code_Char" > The error(s) above occurred for theory "HOL-Library.Code_Char" > (required by "FOL_Harrison.FOL_Harrison") (line 14 of > "/Users/lp15/isabelle/afp/devel/thys/FOL_Harrison/FOL_Harrison.thy") > No such file: "HOL-Library.Code_Char" > The error(s) above occurred in session "FOL_Harrison" (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/FOL_Harrison/ROOT") > Cannot load theory "HOL-Library.Code_Char" > The error(s) above occurred for theory "HOL-Library.Code_Char" > (required by "LTL.LTL_Example") (line 9 of > "/Users/lp15/isabelle/afp/devel/thys/LTL/example/LTL_Example.thy") > No such file: "HOL-Library.Code_Char" > The error(s) above occurred in session "LTL" (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/LTL/ROOT") > Cannot load theory "HOL-Library.Code_Char" > The error(s) above occurred for theory "HOL-Library.Code_Char" > (required by "LLL_Factorization.Modern_Computer_Algebra_Problem") (line 13 of > "/Users/lp15/isabelle/afp/devel/thys/LLL_Factorization/Modern_Computer_Algebra_Problem.thy") > No such file: "HOL-Library.Code_Char" > The error(s) above occurred in session "LLL_Factorization" (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/LLL_Factorization/ROOT") > Cannot load theory "HOL-Library.Code_Char" > The error(s) above occurred for theory "HOL-Library.Code_Char" > (required by "Native_Word.Native_Cast") (line 8 of > "/Users/lp15/isabelle/afp/devel/thys/Native_Word/Native_Cast.thy") > No such file: "HOL-Library.Code_Char" > The error(s) above occurred in session "Native_Word" (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/Native_Word/ROOT") > Cannot load theory "HOL-Library.Code_Char" > The error(s) above occurred for theory "HOL-Library.Code_Char" > (required by "CAVA_Base.CAVA_Base" via "CAVA_Base.CAVA_Code_Target" via > "CAVA_Base.Code_String") (line 9 of > "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy") > No such file: "HOL-Library.Code_Char" > The error(s) above occurred in session "CAVA_Base" (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/ROOT") > Cannot load theory "HOL-Library.Code_Char" > The error(s) above occurred for theory "HOL-Library.Code_Char" > (required by "Transition_Systems_and_Automata.NBA_Explicit" via > "Transition_Systems_and_Automata.NBA_Nodes" via > "DFS_Framework.Reachable_Nodes" via "DFS_Framework.DFS_Framework" via > "DFS_Framework.Param_DFS" via "CAVA_Base.CAVA_Base" via > "CAVA_Base.CAVA_Code_Target" via "CAVA_Base.Code_String") (line 9 of > "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy") > No such file: "HOL-Library.Code_Char" > The error(s) above occurred in session "Transition_Systems_and_Automata" > (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/Transition_Syste
[isabelle-dev] Bad session structure: may cause problems with theory imports
In the past couple of days, upon launching Isabelle jEdit, I get an alert box with the message above and the attached text. Any ideas? Larry ~/isabelle/Repos/src/Pure: hg id 362baebe25a5 tip Cannot load theory "HOL-Library.Code_Char" The error(s) above occurred for theory "HOL-Library.Code_Char" (required by "Affine_Arithmetic.Affine_Arithmetic" via "Affine_Arithmetic.Ex_Affine_Approximation" via "Affine_Arithmetic.Print") (line 8 of "/Users/lp15/isabelle/afp/devel/thys/Affine_Arithmetic/Print.thy") No such file: "HOL-Library.Code_Char" The error(s) above occurred in session "HOL-ODE-Refinement" (line 19 of "/Users/lp15/isabelle/afp/devel/thys/Ordinary_Differential_Equations/ROOT") Cannot load theory "HOL-Library.Code_Char" The error(s) above occurred for theory "HOL-Library.Code_Char" (required by "JinjaThreads.Basic_Main") (line 5 of "/Users/lp15/isabelle/afp/devel/thys/JinjaThreads/Basic/Basic_Main.thy") No such file: "HOL-Library.Code_Char" The error(s) above occurred in session "JinjaThreads" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/JinjaThreads/ROOT") Cannot load theory "HOL-Library.Code_Char" The error(s) above occurred for theory "HOL-Library.Code_Char" (required by "DFS_Framework.DFS_Framework" via "DFS_Framework.Param_DFS" via "CAVA_Base.CAVA_Base" via "CAVA_Base.CAVA_Code_Target" via "CAVA_Base.Code_String") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy") No such file: "HOL-Library.Code_Char" The error(s) above occurred in session "Maxflow_Lib" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Flow_Networks/ROOT") Cannot load theory "HOL-Library.Code_Char" The error(s) above occurred for theory "HOL-Library.Code_Char" (line 14 of "/Users/lp15/isabelle/afp/devel/thys/Iptables_Semantics/ROOT") No such file: "HOL-Library.Code_Char" The error(s) above occurred in session "Iptables_Semantics" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Iptables_Semantics/ROOT") Cannot load theory "HOL-Library.Code_Char" The error(s) above occurred for theory "HOL-Library.Code_Char" (required by "FOL_Harrison.FOL_Harrison") (line 14 of "/Users/lp15/isabelle/afp/devel/thys/FOL_Harrison/FOL_Harrison.thy") No such file: "HOL-Library.Code_Char" The error(s) above occurred in session "FOL_Harrison" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/FOL_Harrison/ROOT") Cannot load theory "HOL-Library.Code_Char" The error(s) above occurred for theory "HOL-Library.Code_Char" (required by "LTL.LTL_Example") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/LTL/example/LTL_Example.thy") No such file: "HOL-Library.Code_Char" The error(s) above occurred in session "LTL" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/LTL/ROOT") Cannot load theory "HOL-Library.Code_Char" The error(s) above occurred for theory "HOL-Library.Code_Char" (required by "LLL_Factorization.Modern_Computer_Algebra_Problem") (line 13 of "/Users/lp15/isabelle/afp/devel/thys/LLL_Factorization/Modern_Computer_Algebra_Problem.thy") No such file: "HOL-Library.Code_Char" The error(s) above occurred in session "LLL_Factorization" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/LLL_Factorization/ROOT") Cannot load theory "HOL-Library.Code_Char" The error(s) above occurred for theory "HOL-Library.Code_Char" (required by "Native_Word.Native_Cast") (line 8 of "/Users/lp15/isabelle/afp/devel/thys/Native_Word/Native_Cast.thy") No such file: "HOL-Library.Code_Char" The error(s) above occurred in session "Native_Word" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Native_Word/ROOT") Cannot load theory "HOL-Library.Code_Char" The error(s) above occurred for theory "HOL-Library.Code_Char" (required by "CAVA_Base.CAVA_Base" via "CAVA_Base.CAVA_Code_Target" via "CAVA_Base.Code_String") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy") No such file: "HOL-Library.Code_Char" The error(s) above occurred in session "CAVA_Base" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/ROOT") Cannot load theory "HOL-Library.Code_Char" The error(s) above occurred for theory "HOL-Library.Code_Char" (required by "Transition_Systems_and_Automata.NBA_Explicit" via "Transition_Systems_and_Automata.NBA_Nodes" via "DFS_Framework.Reachable_Nodes" via "DFS_Framework.DFS_Framework" via "DFS_Framework.Param_DFS" via "CAVA_Base.CAVA_Base" via "CAVA_Base.CAVA_Code_Target" via "CAVA_Base.Code_String") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy") No such file: "HOL-Library.Code_Char" The error(s) above occurred in session "Transition_Systems_and_Automata" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Transition_Systems_and_Automata/ROOT") Cannot load theory "HOL-Library.Code_Char" The error(s) above occurred for theory "HOL-Library.Code_Char" (required by "Knuth_Morris_Pratt.KMP") (line 4 of "/Users/lp15/isabelle/afp/devel/thys/Knuth_Morris_Pratt/KMP.thy") No such file: "HOL-Library.Code_Char" The error(s) above occurred in session
