Re: [isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc
On 18/06/18 21:30, Lars Hupel wrote: > > the good news is that we have just received new hardware (Dual Epyc 7601). > > The bad news is that a current development snapshot > (Isabelle/410818a69ee3) exhibits a problem on this hardware. In > particular, the session HOL-Corec_Examples doesn't appear to terminate. > > The precise invocation is: > > $ ./isabelle/bin/isabelle build -cbv -a -o threads=2 -j 16 > > Isabelle2017 "build -bva" works fine. This qualifies the problem as a > regression, I suppose. Isabelle2017 still uses Poly/ML 5.6, but for the coming release we are on 5.7.1, which is quite different in many respects. > - The "poly" process gets stuck at 100% CPU load and keeps calling "mmap" > - When trying to build the nonterminating session without "-b", it > terminates > - GDB tells me the following stack trace when "mmap" is called (which > corroborates that it happens during heap dumping): > > #0 0x7f8dab80ba13 in __GI___mmap64 (addr=0x0, len=32768, prot=7, > flags=34, fd=-1, offset=0) at ../sysdeps/unix/sysv/linux/mmap64.c:52 > #1 0x00879d56 in OSMem::Allocate(unsigned long&, unsigned int) () > #2 0x00871c6e in MemMgr::NewExportSpace(unsigned long, bool, > bool, bool) () > #3 0x0085f020 in CopyScan::ScanAddressAt(PolyWord*) () > #4 0x0088c2b6 in > ScanAddress::ScanAddressesInObject(PolyObject*, unsigned long) () > ... > #24 0x0088c335 in > ScanAddress::ScanAddressesInObject(PolyObject*, unsigned long) () > #25 0x0088c8c1 in ScanAddress::ScanAddressesInRegion(PolyWord*, > PolyWord*) () > #26 0x008890a1 in SaveRequest::Perform() () > #27 0x00882717 in Processes::BeginRootThread(PolyObject*) () > #28 0x00874a9c in polymain () > #29 0x7f8dab711b97 in __libc_start_main (main=0x405720 , > argc=16, argv=0x7fffe693d4d8, init=, fini= out>, rtld_fini=, stack_end=0x7fffe693d4c8) at > ../csu/libc-start.c:310 > #30 0x00405e01 in _start () David Matthews is the only one who can address this. Maybe the problem is even related to the non-termination we've seen recently on HOL-Proofs. > I'm open to any suggestions for how to diagnose this. Happy to give out > SSH access to the machine. Of course, I have also use for such a machine for testing Isabelle + AFP as usual. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc
Dear list, the good news is that we have just received new hardware (Dual Epyc 7601). The bad news is that a current development snapshot (Isabelle/410818a69ee3) exhibits a problem on this hardware. In particular, the session HOL-Corec_Examples doesn't appear to terminate. $ cat .isabelle/etc/settings init_components "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main" ML_OPTIONS="-H 4000 --maxheap 8G" ML_PLATFORM="$ISABELLE_PLATFORM64" ML_HOME="$POLYML_HOME/$ML_PLATFORM" ISABELLE_GHC=ghc ISABELLE_POLYML="$ML_HOME/poly" ISABELLE_SCALA="$SCALA_HOME/bin" ISABELLE_OCAMLC=ocamlc ISABELLE_OCAML=ocaml ISABELLE_MLTON=mlton ISABELLE_SWIPL=swipl ISABELLE_SMLNJ=sml The precise invocation is: $ ./isabelle/bin/isabelle build -cbv -a -o threads=2 -j 16 Isabelle2017 "build -bva" works fine. This qualifies the problem as a regression, I suppose. I've done some preliminary tracing; here are my findings: - The "poly" process gets stuck at 100% CPU load and keeps calling "mmap" - When trying to build the nonterminating session without "-b", it terminates - GDB tells me the following stack trace when "mmap" is called (which corroborates that it happens during heap dumping): #0 0x7f8dab80ba13 in __GI___mmap64 (addr=0x0, len=32768, prot=7, flags=34, fd=-1, offset=0) at ../sysdeps/unix/sysv/linux/mmap64.c:52 #1 0x00879d56 in OSMem::Allocate(unsigned long&, unsigned int) () #2 0x00871c6e in MemMgr::NewExportSpace(unsigned long, bool, bool, bool) () #3 0x0085f020 in CopyScan::ScanAddressAt(PolyWord*) () #4 0x0088c2b6 in ScanAddress::ScanAddressesInObject(PolyObject*, unsigned long) () ... #24 0x0088c335 in ScanAddress::ScanAddressesInObject(PolyObject*, unsigned long) () #25 0x0088c8c1 in ScanAddress::ScanAddressesInRegion(PolyWord*, PolyWord*) () #26 0x008890a1 in SaveRequest::Perform() () #27 0x00882717 in Processes::BeginRootThread(PolyObject*) () #28 0x00874a9c in polymain () #29 0x7f8dab711b97 in __libc_start_main (main=0x405720 , argc=16, argv=0x7fffe693d4d8, init=, fini=out>, rtld_fini=, stack_end=0x7fffe693d4c8) at ../csu/libc-start.c:310 #30 0x00405e01 in _start () I'm open to any suggestions for how to diagnose this. Happy to give out SSH access to the machine. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] quaternions
To me, the first application of cross products that crosses my mind is vector analysis; it can help define concepts like the curl. Thus, if it is not a separate AFP entry, I think it might fit in analysis. Mohammad On Mon, Jun 18, 2018 at 2:24 PM, wrote: > Send isabelle-dev mailing list submissions to > isabelle-dev@mailbroy.informatik.tu-muenchen.de > > To subscribe or unsubscribe via the World Wide Web, visit > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > or, via email, send a message with subject or body 'help' to > isabelle-dev-requ...@mailbroy.informatik.tu-muenchen.de > > You can reach the person managing the list at > isabelle-dev-ow...@mailbroy.informatik.tu-muenchen.de > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of isabelle-dev digest..." > > > Today's Topics: > >1. quaternions (Lawrence Paulson) >2. Re: quaternions (Lars Hupel) >3. Re: quaternions (Tobias Nipkow) >4. Re: quaternions (Manuel Eberl) > > > -- > > Message: 1 > Date: Mon, 18 Jun 2018 11:36:58 +0100 > From: Lawrence Paulson > To: Isabelle-dev list > , Johannes H?lzl > > Subject: [isabelle-dev] quaternions > Message-ID: <5b41a03d-65ae-4a0f-b5d2-d405caede...@cam.ac.uk> > Content-Type: text/plain; charset=us-ascii > > I have just formalised most of the HOL Light development of quaternions. It's > a great advertisement for type classes: showing that quaternions constitute a > real normed division algebra and an inner product space supersedes most of > the HOL Light proofs (many files), which are devoted to developing the > arithmetic and topological properties of quaternions. In the course of this, > I also ported the HOL Light development of the three-dimensional vector cross > product. > > So where does this material belong? Arguably not in Analysis, which is > already too large. > > Another question: I did not port the quaternion material relating to the > constant reflect_along, which is defined as follows: > > (* Reflection of a vector about 0 along a line. *) > > let reflect_along = new_definition > `reflect_along v (x:real^N) = x - (&2 * (x dot v) / (v dot v)) % v`;; > > Is this concept useful, and if so, where does it belong? > > Larry > > > > -- > > Message: 2 > Date: Mon, 18 Jun 2018 14:17:34 +0200 > From: Lars Hupel > To: Lawrence Paulson , Isabelle-dev list > , Johannes H?lzl > > Subject: Re: [isabelle-dev] quaternions > Message-ID: > Content-Type: text/plain; charset=utf-8 > >> So where does this material belong? Arguably not in Analysis, which is >> already too large. > > Why not a regular AFP entry? > > Cheers > Lars > > > -- > > Message: 3 > Date: Mon, 18 Jun 2018 14:18:08 +0200 > From: Tobias Nipkow > To: isabelle-dev@mailbroy.informatik.tu-muenchen.de > Subject: Re: [isabelle-dev] quaternions > Message-ID: <50edc647-c34c-057c-4c02-471dac7ce...@in.tum.de> > Content-Type: text/plain; charset="utf-8"; Format="flowed" > > Why not simply the AFP? > > Tobias > > On 18/06/2018 12:36, Lawrence Paulson wrote: >> I have just formalised most of the HOL Light development of quaternions. >> It's a great advertisement for type classes: showing that quaternions >> constitute a real normed division algebra and an inner product space >> supersedes most of the HOL Light proofs (many files), which are devoted to >> developing the arithmetic and topological properties of quaternions. In the >> course of this, I also ported the HOL Light development of the >> three-dimensional vector cross product. >> >> So where does this material belong? Arguably not in Analysis, which is >> already too large. >> >> Another question: I did not port the quaternion material relating to the >> constant reflect_along, which is defined as follows: >> >> (* Reflection of a vector about 0 along a line. *) >> >> let reflect_along = new_definition >> `reflect_along v (x:real^N) = x - (&2 * (x dot v) / (v dot v)) % v`;; >> >> Is this concept useful, and if so, where does it belong? >> >> Larry >> >> ___ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> > > -- next part -- >
Re: [isabelle-dev] quaternions
The cross product development is 200 lines long while the quaternion development is 730. Should they be separate entries, or do cross products belong elsewhere? Larry > On 18 Jun 2018, at 13:18, Tobias Nipkow wrote: > > Why not simply the AFP? signature.asc Description: Message signed with OpenPGP ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] quaternions
I would also have suggested an AFP entry. > let reflect_along = new_definition > `reflect_along v (x:real^N) = x - (&2 * (x dot v) / (v dot v)) % v`;; Think of it as x being the direction of a ray of light hitting a mirror (in the shape of a hyperplane through the origin with normal vector a) and being reflected. The result is the direction of the reflected ray. Where it belongs I cannot say; that depends on what kinds of results are proven about it. I for one would consider this a very ‘applied’ concept (I know it from ray tracing), so unless we have a concrete application for it, I'm not sure we need it at all. Manuel On 2018-06-18 14:17, Lars Hupel wrote: >> So where does this material belong? Arguably not in Analysis, which is >> already too large. > Why not a regular AFP entry? > > Cheers > Lars > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] quaternions
Why not simply the AFP? Tobias On 18/06/2018 12:36, Lawrence Paulson wrote: I have just formalised most of the HOL Light development of quaternions. It's a great advertisement for type classes: showing that quaternions constitute a real normed division algebra and an inner product space supersedes most of the HOL Light proofs (many files), which are devoted to developing the arithmetic and topological properties of quaternions. In the course of this, I also ported the HOL Light development of the three-dimensional vector cross product. So where does this material belong? Arguably not in Analysis, which is already too large. Another question: I did not port the quaternion material relating to the constant reflect_along, which is defined as follows: (* Reflection of a vector about 0 along a line. *) let reflect_along = new_definition `reflect_along v (x:real^N) = x - (&2 * (x dot v) / (v dot v)) % v`;; Is this concept useful, and if so, where does it belong? Larry ___ 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
Re: [isabelle-dev] quaternions
> So where does this material belong? Arguably not in Analysis, which is > already too large. Why not a regular AFP entry? Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] quaternions
I have just formalised most of the HOL Light development of quaternions. It's a great advertisement for type classes: showing that quaternions constitute a real normed division algebra and an inner product space supersedes most of the HOL Light proofs (many files), which are devoted to developing the arithmetic and topological properties of quaternions. In the course of this, I also ported the HOL Light development of the three-dimensional vector cross product. So where does this material belong? Arguably not in Analysis, which is already too large. Another question: I did not port the quaternion material relating to the constant reflect_along, which is defined as follows: (* Reflection of a vector about 0 along a line. *) let reflect_along = new_definition `reflect_along v (x:real^N) = x - (&2 * (x dot v) / (v dot v)) % v`;; Is this concept useful, and if so, where does it belong? Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
