Re: [isabelle-dev] Deadlock while building HOL-Proof
On 10/03/18 11:06, Makarius wrote: > On 08/03/18 13:08, Makarius wrote: >> >>> Since David Matthews has make a lot of changes concerning fine-points of >>> heap management in the past few months, I would like to test it with >>> some Poly/ML repository version. But this does not build on macOS at the >>> moment. >> >> I will continue with the investigations here. > > I have now tested it with various experimental versions of Poly/ML: the > problem persists. > > Looking more closely at the ML statistics of the process (after killing > it) reveals that the ML world is fine and active, only my future thread > farm is somehow blocked. > > This indicates that the problem is in my area of responsibility. In the past couple of weeks I have sporadically tried to work around this resource problem, but failed so far. The latest attempt is Isabelle/f6a22490cca8. As usual, it "works for me on my usual test machines", but there is a remaining chance of problems coming back on other configurations. Overall, my guess is that the Poly/ML parallel GC vs. Isabelle/ML future thread management somehow get into trouble, due to massive resource requirements in parallel HOL-Proofs with a sudden spike of approx. 5 futures that require a lot of memory. Even x86_64 does not really help. In a sense, it is just the normal situation "invisible concrete wall ahead" -- we've that had occasionally in the past 10-20 years. It is a reminder that scaling is not for free, but explicit efforts are required for it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle server
On 26/03/18 13:48, Christian Sternagel wrote: > > Thanks, I forgot about that option. > > With "isabelle latex" in the specified directory the error boils down to: > > ./root.tex:31: Package pdftex.def Error: File > `isabelle-eps-converted-to.pdf' n > ot found. > > See the pdftex.def package documentation for explanation. > Type H for immediate help. > ... > > Should isabelle-eps-converted-to.pdf exist on my system? I guess that the "epstopdf" tool is missing: there should be some Fedora package for it. Anyway, in Isabelle/2a5ae592eafb the latex errors are again spilled into user output -- this is required for hard errors of missing executables and style files. With that I have managed to do "isabelle build -o document=pdf -g doc" or "isabelle build_doc -a" sucessfully on Fedora 28: after cumbersome saturation of the texlive installation, where almost every style file has its own package. Makarius ___ 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
