Re: [isabelle-dev] Analysis not building

2019-02-03 Thread Bertram Felgenhauer
Florian Haftmann wrote:
> > HOL-Analysis can’t be built (reproducibly) with the latest version 
> > (76f2d492627e). It simply dies, no error message.
> 
> I cannot reproduce this.

Neither can I; using polyml-b68438d33c69 I can build HOL-Analysis
with Isabelle-24bbc4e30e5b and manual init-component for Poly/ML and
both HOL-Analysis and IsaFoR with Isabelle-2018 and the same manual
init-component.

Maybe this is somehow specific to OS/X, which I believe Larry uses?

That said, polyml-1b2dcf8f5202 seems to work just as well, for me. 

In other news, the problem with the sharing pass appears to be resolved
and the IsaFoR images with x86_64_32 are now all about 60% the size of
the x86_64 ones. Nice!

Cheers,

Bertram

Numbers:

ML_PLATFORM="x86_64_32-linux"
ML_OPTIONS="--maxheap 16G -H 500 --gcthreads 6"
ISABELLE_BUILD_OPTIONS="threads=10 parallel_proofs=2"

polyml-test-1b2dcf8f5202
polyml-test-b68438d33c69


Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14)
Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14)

Finished HOL (0:02:23 elapsed time, 0:08:49 cpu time, factor 3.68)
Finished HOL (0:02:26 elapsed time, 0:08:58 cpu time, factor 3.69)

Finished HOL-Lib (0:05:12 elapsed time, 0:32:06 cpu time, factor 6.17)
Finished HOL-Lib (0:04:58 elapsed time, 0:31:08 cpu time, factor 6.25)

Finished HOL-AFP (0:05:40 elapsed time, 0:32:52 cpu time, factor 5.79)
Finished HOL-AFP (0:05:38 elapsed time, 0:32:51 cpu time, factor 5.82)

Finished IsaFoR_1 (0:05:10 elapsed time, 0:27:31 cpu time, factor 5.32)
Finished IsaFoR_1 (0:05:11 elapsed time, 0:27:39 cpu time, factor 5.33)

Finished IsaFoR_2 (0:05:26 elapsed time, 0:25:37 cpu time, factor 4.71)
Finished IsaFoR_2 (0:05:27 elapsed time, 0:25:37 cpu time, factor 4.69)

Finished IsaFoR_3 (0:06:38 elapsed time, 0:39:22 cpu time, factor 5.92)
Finished IsaFoR_3 (0:06:36 elapsed time, 0:39:24 cpu time, factor 5.96)

Finished IsaFoR_4 (0:08:26 elapsed time, 0:26:28 cpu time, factor 3.14)
Finished IsaFoR_4 (0:08:37 elapsed time, 0:26:55 cpu time, factor 3.12)

Finished Code (0:08:03 elapsed time, 0:08:11 cpu time, factor 1.02)
Finished Code (0:08:02 elapsed time, 0:08:11 cpu time, factor 1.02)

 19271289 Pure (0.69 x 28081037 (x86_64 heap image size))
 19269857 Pure (0.69)

250024211 HOL (0.61 x 410972244)
250129275 HOL (0.61)

307851090 HOL-Lib (0.59 x 525949867)
307921910 HOL-Lib (0.59)

537798522 HOL-AFP (0.59 x 913422879)
537694918 HOL-AFP (0.59)

428162386 IsaFoR_1 (0.59 x 724672759)
427425094 IsaFoR_1 (0.59)

367783763 IsaFoR_2 (0.59 x 623083120)
367626511 IsaFoR_2 (0.59)

419599023 IsaFoR_3 (0.59 x 712211696)
419246195 IsaFoR_3 (0.59)

284804855 IsaFoR_4 (0.59 x 480209352)
284701607 IsaFoR_4 (0.59)
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-28 Thread Bertram Felgenhauer
Makarius wrote:
> There was indeed something odd with sharing: David Matthews has changed
> that in polyml-1b2dcf8f5202 (see Isabelle/bb0a354f6b46).

I may give it another try later...

> > Hardware:
> >   i7-6850K CPU @ 3.60GHz (6 cores x 2 hyperthreads) / 32GB RAM / SSD
> > 
> > Common build flags:
> >   ISABELLE_BUILD_OPTIONS="threads=12 parallel_proofs=2"
> > 
> > Configurations:
> >   polyml 5.7.1x86_64ML_OPTIONS="--maxheap 24G -H 500 
> > --gcthreads 6"
> >   polyml-a444f281ccec x86_64ML_OPTIONS="--maxheap 24G -H 500 
> > --gcthreads 6"
> 
> For this hardware I recommend threads=6.

In the sessions beyond HOL, I see a speedup from threads=12. The timings
are basically the same with threads=10, but I have not checked the full
range of possibilities.

I've made sure that the machine is mostly idle; things will be much
different if several processes start competing for the ressources.

Configurations:
  threads=6
  threads=10
  threads=12

Times:
  Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.12)
  Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14)
  Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14)
  
  Finished HOL (0:02:21 elapsed time, 0:07:47 cpu time, factor 3.30)
  Finished HOL (0:02:25 elapsed time, 0:08:56 cpu time, factor 3.68)
  Finished HOL (0:02:32 elapsed time, 0:09:46 cpu time, factor 3.84)
  
  Finished HOL-Lib (0:05:47 elapsed time, 0:25:18 cpu time, factor 4.37)
  Finished HOL-Lib (0:05:12 elapsed time, 0:32:29 cpu time, factor 6.24)
  Finished HOL-Lib (0:05:10 elapsed time, 0:35:32 cpu time, factor 6.88)
  
  Finished HOL-AFP (0:06:33 elapsed time, 0:27:55 cpu time, factor 4.26)
  Finished HOL-AFP (0:05:51 elapsed time, 0:34:10 cpu time, factor 5.83)
  Finished HOL-AFP (0:05:41 elapsed time, 0:35:44 cpu time, factor 6.28)
  
  Finished IsaFoR_1 (0:05:11 elapsed time, 0:22:30 cpu time, factor 4.34)
  Finished IsaFoR_1 (0:05:04 elapsed time, 0:27:15 cpu time, factor 5.38)
  Finished IsaFoR_1 (0:05:21 elapsed time, 0:29:58 cpu time, factor 5.59)
  
  Finished IsaFoR_2 (0:05:57 elapsed time, 0:21:49 cpu time, factor 3.66)
  Finished IsaFoR_2 (0:05:43 elapsed time, 0:26:24 cpu time, factor 4.61)
  Finished IsaFoR_2 (0:05:40 elapsed time, 0:27:39 cpu time, factor 4.87)
  
  Finished IsaFoR_3 (0:07:13 elapsed time, 0:31:05 cpu time, factor 4.30)
  Finished IsaFoR_3 (0:06:51 elapsed time, 0:40:15 cpu time, factor 5.87)
  Finished IsaFoR_3 (0:06:45 elapsed time, 0:43:32 cpu time, factor 6.45)
  
  Finished IsaFoR_4 (0:08:37 elapsed time, 0:24:58 cpu time, factor 2.90)
  Finished IsaFoR_4 (0:08:48 elapsed time, 0:27:08 cpu time, factor 3.08)
  Finished IsaFoR_4 (0:08:47 elapsed time, 0:27:52 cpu time, factor 3.17)
  
  Finished Code (0:08:04 elapsed time, 0:08:12 cpu time, factor 1.02)
  Finished Code (0:08:00 elapsed time, 0:08:08 cpu time, factor 1.02)
  Finished Code (0:07:59 elapsed time, 0:08:08 cpu time, factor 1.02)

> Moreover note that --gcthreads is automatically provided, if ML_OPTIONS
> does not say anything else.

I intended to experiment with smaller numbers but have not yet done so.
On another, similar machine, --gcthreads=2 was just as fast as 6.

Cheers,

Bertram
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-25 Thread Bertram Felgenhauer
Bertram Felgenhauer wrote:
> Makarius wrote:
> > So this is the right time for further testing of applications:
> > Isabelle2018 should work as well, but I have not done any testing beyond
> > "isabelle build -g main" -- Isabelle development only moves forward in
> > one direction on a single branch.
>
> I have tried this with Isabelle2018 and IsaFoR; I've encountered no
> problems and there's a nice speedup (estimated 1.25 times faster).
> Heap images are 40% smaller, which is a welcome change as well.

I have gathered some more data (below). There are some curiosities:

- Code export (that's the only thing that the 'Code' session does,
  besides theory merges) seems to be slower with polyml-a444f281ccec
  compared to polyml 5.7.1, even when sticking to the x86_64 platform.

- A similar slowdown seems to affect the IsaFoR_3 session, but I don't
  know what's special about that one.

- While most heap images are about 40% smaller with x86_64_32, this is
  not always the case; some heap images ended up being even larger in
  this experiment. Could there be a problem with the sharing pass on
  x86_64_32?

Cheers,

Bertram

Hardware:
  i7-6850K CPU @ 3.60GHz (6 cores x 2 hyperthreads) / 32GB RAM / SSD

Software:
  GNU/Linux
  Isabelle2018
  afp-2018 @ 400c722462b3
  IsaFoR @ acb9096ce08a

Common build flags:
  ISABELLE_BUILD_OPTIONS="threads=12 parallel_proofs=2"

Configurations:
  polyml 5.7.1x86_64ML_OPTIONS="--maxheap 24G -H 500 --gcthreads 6"
  polyml-a444f281ccec x86_64ML_OPTIONS="--maxheap 24G -H 500 --gcthreads 6"
  polyml-0a6ebca445fc x86_64_32 ML_OPTIONS="--maxheap 16G -H 500 --gcthreads 6"
  polyml-a444f281ccec x86_64_32 ML_OPTIONS="--maxheap 16G -H 500 --gcthreads 6"

Timings:
  Finished Pure (0:00:11 elapsed time, 0:00:14 cpu time, factor 1.20)
  Finished Pure (0:00:15 elapsed time, 0:00:17 cpu time, factor 1.18)
  Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14)
  Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.13)

  Finished HOL (0:02:46 elapsed time, 0:10:50 cpu time, factor 3.91)
  Finished HOL (0:02:41 elapsed time, 0:10:05 cpu time, factor 3.75)
  Finished HOL (0:02:32 elapsed time, 0:09:46 cpu time, factor 3.84)
  Finished HOL (0:02:28 elapsed time, 0:09:20 cpu time, factor 3.78)

  Finished HOL-Lib (0:05:00 elapsed time, 0:35:54 cpu time, factor 7.18)
  Finished HOL-Lib (0:05:19 elapsed time, 0:36:41 cpu time, factor 6.88)
  Finished HOL-Lib (0:05:10 elapsed time, 0:35:32 cpu time, factor 6.88)
  Finished HOL-Lib (0:04:57 elapsed time, 0:34:16 cpu time, factor 6.91)

  Finished HOL-AFP (0:05:59 elapsed time, 0:37:39 cpu time, factor 6.28)
  Finished HOL-AFP (0:06:15 elapsed time, 0:38:31 cpu time, factor 6.15)
  Finished HOL-AFP (0:05:41 elapsed time, 0:35:44 cpu time, factor 6.28)
  Finished HOL-AFP (0:05:33 elapsed time, 0:35:01 cpu time, factor 6.30)

  Finished IsaFoR_1 (0:05:46 elapsed time, 0:31:43 cpu time, factor 5.49)
  Finished IsaFoR_1 (0:05:42 elapsed time, 0:31:06 cpu time, factor 5.46)
  Finished IsaFoR_1 (0:05:21 elapsed time, 0:29:58 cpu time, factor 5.59)
  Finished IsaFoR_1 (0:05:17 elapsed time, 0:29:15 cpu time, factor 5.54)

  Finished IsaFoR_2 (0:06:07 elapsed time, 0:29:37 cpu time, factor 4.84)
  Finished IsaFoR_2 (0:06:04 elapsed time, 0:29:15 cpu time, factor 4.82)
  Finished IsaFoR_2 (0:05:40 elapsed time, 0:27:39 cpu time, factor 4.87)
  Finished IsaFoR_2 (0:05:59 elapsed time, 0:28:14 cpu time, factor 4.72)

  Finished IsaFoR_3 (0:07:30 elapsed time, 0:47:56 cpu time, factor 6.38)
  Finished IsaFoR_3 (0:09:58 elapsed time, 0:55:27 cpu time, factor 5.56) ?
  Finished IsaFoR_3 (0:06:45 elapsed time, 0:43:32 cpu time, factor 6.45)
  Finished IsaFoR_3 (0:06:49 elapsed time, 0:43:20 cpu time, factor 6.35)

  Finished IsaFoR_4 (0:09:40 elapsed time, 0:30:25 cpu time, factor 3.15)
  Finished IsaFoR_4 (0:09:14 elapsed time, 0:29:16 cpu time, factor 3.17)
  Finished IsaFoR_4 (0:08:47 elapsed time, 0:27:52 cpu time, factor 3.17)
  Finished IsaFoR_4 (0:08:52 elapsed time, 0:27:57 cpu time, factor 3.15)

  Finished Code (0:05:30 elapsed time, 0:05:42 cpu time, factor 1.03)
  Finished Code (0:08:34 elapsed time, 0:08:46 cpu time, factor 1.02) ?
  Finished Code (0:07:59 elapsed time, 0:08:08 cpu time, factor 1.02)
  Finished Code (0:08:00 elapsed time, 0:08:08 cpu time, factor 1.02)

  total 00:48:29
  total 00:54:02
  total 00:48:08
  total 00:48:08

Heap image sizes (factor):
   28081037 Pure (1.00)
   25131549 Pure (0.89)
   19271077 Pure (0.68)
   19270685 Pure (0.68)

  410972244 HOL (1.00)
  403934084 HOL (0.98)
  249583659 HOL (0.61)
  249808871 HOL (0.61)

  525949867 HOL-Lib (1.00)
  526132427 HOL-Lib (1.00)
  308088218 HOL-Lib (0.59)
  307456194 HOL-Lib (0.58)

  913422879 HOL-AFP (1.00)
  915450415 HOL-AFP (1.00)
  537947934 HOL-AFP (0.59)
  538445922 HOL-AFP (0.59)

  724672759 IsaFoR_1 (1.00)
  724822231 

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-23 Thread Bertram Felgenhauer
Makarius wrote:
> On 22/01/2019 12:31, Bertram Felgenhauer wrote:
> > Makarius wrote:
> >> So this is the right time for further testing of applications:
> >> Isabelle2018 should work as well, but I have not done any testing beyond
> >> "isabelle build -g main" -- Isabelle development only moves forward in
> >> one direction on a single branch.
> > 
> > I have tried this with Isabelle2018 and IsaFoR; I've encountered no
> > problems and there's a nice speedup (estimated 1.25 times faster).
> > Heap images are 40% smaller, which is a welcome change as well.
> 
> Is that compared to x86_64 (full 64-bit) or x86 (old 32-bit)?

This is compared to x86_64. Sorry, I should have mentioned this,
but to my mind it was implied because IsaFoR is notorious for running
out of memory with the x86 version of PolyML.

> I am asking this, because I have noted a speedup of building heap
> images: x86_64_32 compared to x86, and was wondering about the reasons
> for it. (For x86_64 everything is just more bulky, of course, including
> heaps.)

As far as I can see, one difference between x86 and x86_64_32 is that
PolyML keeps heap objects aligned to 8 byte boundaries for the latter.
This may impact performance.

Cheers,

Bertram
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Bertram Felgenhauer
Makarius wrote:
> So this is the right time for further testing of applications:
> Isabelle2018 should work as well, but I have not done any testing beyond
> "isabelle build -g main" -- Isabelle development only moves forward in
> one direction on a single branch.

I have tried this with Isabelle2018 and IsaFoR; I've encountered no
problems and there's a nice speedup (estimated 1.25 times faster).
Heap images are 40% smaller, which is a welcome change as well.

Thanks a lot, David and Makarius!

Bertram
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] NEWS: support for GHC

2018-11-08 Thread Bertram Felgenhauer
Makarius wrote:
> On 08/11/2018 14:59, Bertram Felgenhauer wrote:
> >>
> >> I've misunderstood the problem. You intend to invoke old-style
> >> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
> >> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.
> > 
> > This may be premature, but I foresee that now that `isabelle ghc`
> > and `isabelle ghci` exist, we will have scripts that use them.
> 
> There is indeed some confusion here.
> 
> My reluctance to execute $ISABELLE_GHC inside lib/Tools/ghc is explained
> by the odd recursive setup: in the stack situation, $ISABELLE_GHC points
> to lib/Tools/ghc, and some mistake in the configuration could lead to
> infinite recursion of sub-processes (potential bombing of the OS).
> 
> It is probably better to leave the meaning of ISABELLE_GHC (and
> ISABELLE_OCAML, ISABELLE_OCAMLC) unchanged, and remove the "isabelle
> ghc" tool entry points: these auxiliary scripts should go into
> $ISABELLE_HOME/lib/scripts where they cannot be mistaken as regular
> Isabelle tools.

Sounds good to me.

Cheers,

Bertram

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] NEWS: support for GHC

2018-11-08 Thread Bertram Felgenhauer
Makarius wrote:
> On 08/11/2018 11:30, Bertram Felgenhauer wrote:
> > Makarius wrote:
> >> Nonetheless, it is still possible to use "isabelle ghc" without stack:
> >> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
> >> Isabelle settings mechanism to override ISABELLE_GHC with the
> >> stack-based tools.
> > 
> > After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about
> > a missing GHC setup, since there's no fallback on a custom
> > $ISABELLE_GHC. I've added such a fallback in the attached patch,
> > does that look reasonable?
> 
> I've misunderstood the problem. You intend to invoke old-style
> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.

This may be premature, but I foresee that now that `isabelle ghc`
and `isabelle ghci` exist, we will have scripts that use them.

> So just the usual question: What are remaining uses of this? Why not
> uninstall the "system ghc" and only use stack?

I don't think that the desire of using an existing ghc installation is
unusual. I'm not sure how common maintaining a ghc installation without
stack is these days, but ghc + cabal-install are still quite sufficient
for Haskell development. I don't care much about disk space, but I do
resent stack's propensity for downloading huge tarballs without even
prompting; my bandwidth is often limited. So I try hard to avoid that
particular tool.

> My impression is that up-to-date Haskell projects are all using stack by
> default.

My desire is to be able to override the default, not to change it.

Cheers,

Bertram
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] NEWS: support for GHC

2018-11-08 Thread Bertram Felgenhauer
Makarius wrote:
> Nonetheless, it is still possible to use "isabelle ghc" without stack:
> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
> Isabelle settings mechanism to override ISABELLE_GHC with the
> stack-based tools.

After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about
a missing GHC setup, since there's no fallback on a custom
$ISABELLE_GHC. I've added such a fallback in the attached patch,
does that look reasonable?

Cheers,

Bertram
diff -r 0a9688695a1b lib/Tools/ghc
--- a/lib/Tools/ghc Thu Nov 08 09:11:52 2018 +0100
+++ b/lib/Tools/ghc Thu Nov 08 11:25:55 2018 +0100
@@ -6,6 +6,8 @@
 
 if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then
   isabelle_stack ghc -- "$@"
+elif [ -n "$ISABELLE_GHC" ]; then
+  "$ISABELLE_GHC" "$@"
 else
   echo "Cannot execute ghc: missing Isabelle GHC setup" >&2
   exit 127
diff -r 0a9688695a1b lib/Tools/ghci
--- a/lib/Tools/ghciThu Nov 08 09:11:52 2018 +0100
+++ b/lib/Tools/ghciThu Nov 08 11:25:55 2018 +0100
@@ -6,6 +6,8 @@
 
 if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then
   isabelle_stack ghci "$@"
+elif [ -n "$ISABELLE_GHC" ]; then
+  "$ISABELLE_GHC" --interactive "$@"
 else
   echo "Cannot execute ghci: missing Isabelle GHC setup" >&2
   exit 127
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] NEWS: support for GHC

2018-11-07 Thread Bertram Felgenhauer
Makarius wrote:
> *** System ***
> 
> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
> Existing settings variable ISABELLE_GHC is maintained dynamically
> according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.
> 
> 
> This refers to Isabelle/1722cc56d22e.

Is there a way to use a system ghc with `isabelle ghc` and
`isabelle ghci`? I want to avoid the 145MB download and extra
installation of ghc if possible.

Note in particular that setting ISABELLE_GHC now has a peculiar
effect on `isabelle ghc`. Without the environment variable, the
command complains:

  Cannot execute ghc: missing Isabelle GHC setup

However, if ISABELLE_GHC is set in $ISABELLE_HOME/etc/settings,
then the same command starts downloading ghc via stack...

  > isabelle ghc
  Preparing to install GHC (tinfo6) to an isolated location.
  This will not interfere with any system-level installation.
  Preparing to download ghc-tinfo6-8.4.4 ...^C

Given the size of the download I find this unsatisfactory
(145 MB is still big for mobile plans.)

Cheers,

Bertram
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] [isabelle] Proposal: An update to Multiset theory

2016-08-08 Thread Bertram Felgenhauer
Florian Haftmann wrote:
> Hi Bertram,
> 
> > How shall we proceed? As I hinted at earlier I do not have (nor want, at
> > this point) push access, but I can prepare a patch or clone of the repo,
> > if that helps, or just provide a plain theory file that works with the
> > development version of Isabelle.
> 
> a repo URL or a patch is indeed the best thing to proceed: there is not
> »the« development version but an ongoing agile development.

Okay, I have exported a series of two patches against 1e7c5bbea36d,
the first adding monotonicity lemmata and the second for cancellation
and `multp`, `multeq`. See the attached file.

Cheers,

Bertram
# HG changeset patch
# User Bertram Felgenhauer <bertram.felgenha...@uibk.ac.at>
# Date 1470657709 -7200
#  Mon Aug 08 14:01:49 2016 +0200
# Node ID 852c841c2ecde57bd9d0695edbad5b392ab418b5
# Parent  1e7c5bbea36dd2dd56705630f8e456de91b9788a
add monotonicity propertyies of `mult1` and `mult`

diff -r 1e7c5bbea36d -r 852c841c2ecd src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Aug 07 12:10:49 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Aug 08 14:01:49 2016 +0200
@@ -2214,6 +2214,14 @@
   obtains a M0 K where "M = M0 + {#a#}" "N = M0 + K" "\b. b \# K \ (b, a) \ r"
   using assms unfolding mult1_def by blast
 
+lemma mono_mult1:
+  assumes "r \ r'" shows "mult1 r \ mult1 r'"
+unfolding mult1_def using assms by blast
+
+lemma mono_mult:
+  assumes "r \ r'" shows "mult r \ mult r'"
+unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
+
 lemma not_less_empty [iff]: "(M, {#}) \ mult1 r"
 by (simp add: mult1_def)
 
# HG changeset patch
# User Bertram Felgenhauer <bertram.felgenha...@uibk.ac.at>
# Date 1470657822 -7200
#  Mon Aug 08 14:03:42 2016 +0200
# Node ID 842352253b462144ba8a26e45080f53a1cefe2d8
# Parent  852c841c2ecde57bd9d0695edbad5b392ab418b5
prove monotonicity of `mult1` and `mult`

diff -r 852c841c2ecd -r 842352253b46 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Aug 08 14:01:49 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Aug 08 14:03:42 2016 +0200
@@ -2404,115 +2404,103 @@
 \ (I + K, I + J) \ mult r"
 using one_step_implies_mult_aux by blast
 
-subsection \A quasi-executable characterization\
-
-text \
-  The decreasing parts \A\ and \B\ of multisets in a multiset-comparison
-  \(I + B, I + A) \ mult r\, can always be made disjoint.
-\
-lemma decreasing_parts_disj:
-  assumes "irrefl r" and "trans r"
-and "A \ {#}" and *: "\b\#B. \a\#A. (b, a) \ r"
-  defines "Z \ A #\ B"
-  defines "X \ A - Z"
-  defines "Y \ B - Z"
-  shows "X \ {#} \ X #\ Y = {#} \
-A = X + Z \ B = Y + Z \ (\y\#Y. \x\#X. (y, x) \ r)"
+
+subsection \The multiset extension is cancellative for multiset union\
+
+lemma mult_cancel:
+  assumes "trans s" and "irrefl s"
+  shows "(X + Z, Y + Z) \ mult s \ (X, Y) \ mult s" (is "?L \ ?R")
+proof
+  assume ?L thus ?R
+  proof (induct Z)
+case (add Z z)
+obtain X' Y' Z' where *: "X + Z + {#z#} = Z' + X'" "Y + Z + {#z#} = Z' + Y'" "Y' \ {#}"
+  "\x \ set_mset X'. \y \ set_mset Y'. (x, y) \ s"
+  using mult_implies_one_step[OF `trans s` add(2)] unfolding add.assoc by blast
+consider Z2 where "Z' = Z2 + {#z#}" | X2 Y2 where "X' = X2 + {#z#}" "Y' = Y2 + {#z#}"
+  using *(1,2) by (metis mset_add union_iff union_single_eq_member)
+thus ?case
+proof (cases)
+  case 1 thus ?thesis using * one_step_implies_mult[of Y' X' s Z2]
+by (auto simp: add.commute[of _ "{#_#}"] add.assoc intro: add(1))
+next
+  case 2 then obtain y where "y \ set_mset Y2" "(z, y) \ s" using *(4) `irrefl s`
+by (auto simp: irrefl_def)
+  moreover from this transD[OF `trans s` _ this(2)]
+  have "x' \ set_mset X2 \ \y \ set_mset Y2. (x', y) \ s" for x'
+using 2 *(4)[rule_format, of x'] by auto
+  ultimately show ?thesis using  * one_step_implies_mult[of Y2 X2 s Z'] 2
+by (force simp: add.commute[of "{#_#}"] add.assoc[symmetric] intro: add(1))
+qed
+  qed auto
+next
+  assume ?R then obtain I J K
+where "Y = I + J" "X = I + K" "J \ {#}" "\k \ set_mset K. \j \ set_mset J. (k, j) \ s"
+using mult_implies_one_step[OF `trans s`] by blast
+  thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
+qed
+
+lemma mult_cancel_max:
+  assumes "trans s" and "irrefl s"
+  shows "(X, Y) \ mult s \ (X - X #\ Y, Y - X #\ Y) \ mult s" (is "?L \ ?R")
 proof -
-  define D
-where "D = set_mset A \ set_mset B"
-  let ?r = "r \ 

Re: [isabelle-dev] code abbreviation for mapping over a fixed range

2015-11-07 Thread Bertram Felgenhauer
Hi Florian,
> > This email refers to the following commit:
> > 
> >   http://isabelle.in.tum.de/repos/isabelle/rev/7d1127ac2251
> > 
> >   code abbreviation for mapping over a fixed range
> > 
> > Is there a specific reason for this code equation:
> > 
> >   "map_range f (Suc n) = map_range f n @ [f n]"
> > 
> > It seems rather inefficient. Anyway, what's the purpose of "map_range".
> 
> the idea of map_range is to avoid building a list first and then mapping it.

Please don't forget about this.

The new definition actually causes *more* allocation than the original
one, except for very short lists, because every call of @ copies its
first argument. Note that the code equation for [_..<_] is

  lemma upt_rec[code]: "[i..

Re: [isabelle-dev] AFP devel not reachable

2015-07-20 Thread Bertram Felgenhauer
David Cock wrote:
 Apparently they had a storage system issue, and obviously didn't have a
 tested recovery plan.

There's some more information here:

http://sourceforge.net/blog/sourceforge-infrastructure-and-service-restoration/

In short, they are working on it, and interestingly, they are holding
restoration of SCM services off until last...

 At this point, the sooner everybody moves off of
 Sourceforge, the better.

It'd also be nice to have a mirror of the repository, regardless of where
it's hosted.

Cheers,

Bertram
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


[isabelle-dev] Tweak Haskell output for future Haskell compatibility.

2012-05-07 Thread Bertram Felgenhauer
Dear Isabelle developers,

the Haskell code generator of Isabelle currently emits contexts for
data and newtype generates, e.g. (from CeTA):

  newtype (Linorder a) = Rbt a b = Rbt (Rbta a b);

The sole effect of such contexts is that the programmer must provide
a (Linorder a) context wherever Rbt a b is used, which is fairly uselss.
In the next version of the Haskell language definition (whenever that
will be), this feature will be removed.

  http://www.haskell.org/pipermail/haskell-prime/2011-January/003335.html
  http://hackage.haskell.org/trac/haskell-prime/wiki/NoDatatypeContexts

Ghc currently requires a flag (-XDatatypeContexts) to compile code
using datatype contexts. In the latest release (7.4.1), this option
emits a warning:

Warning: -XDatatypeContexts is deprecated: It was widely considered a
misfeature, and has been removed from the Haskell language.

I propose, therefore, to omit these contexts in code generated by
Isabelle. This can safely wait until after the release, of course.
(patch attached)

Best regards,

Bertram
# HG changeset patch
# User felgenhauer
# Date 1336397766 -7200
# Node ID 1a976d546b94ca265a26f6d916a7f54979c0c547
# Parent  29212a4bb866adc5f8f94a85602acb8dbcd65f81
do not generate contexts for datatype declarations in generated Haskell code
(see http://hackage.haskell.org/trac/haskell-prime/wiki/NoDatatypeContexts)

diff -r 29212a4bb866 -r 1a976d546b94 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Fri May 04 17:12:37 2012 +0200
+++ b/src/Tools/Code/code_haskell.ML	Mon May 07 15:36:06 2012 +0200
@@ -57,7 +57,7 @@
   | SOME (_, print) = print (print_typ tyvars) fxy tys)
   | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
 fun print_typdecl tyvars (vs, tycoexpr) =
-  Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr);
+  print_tyco_expr tyvars NOBR tycoexpr;
 fun print_typscheme tyvars (vs, ty) =
   Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
 fun print_term tyvars some_thm vars fxy (IConst c) =
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Isabelle_11-Sep-2011

2011-09-30 Thread Bertram Felgenhauer
Dear Makarius and René,

 However, testing Isabelle_20-Sep-2011 with Emacs 23.3, there seems to be a 
 problem for Mac OS Lion users:
 Many special characters like == \in, = are not displayed correctly which 
 makes working inconvenient. Under
 
 http://cl-informatik.uibk.ac.at/~thiemann/emacs.html

I believe I know this bug. It's an emacs problem, and should be fixed in
emacs 23.4 once it becomes available. That said I don't know of any elisp
code other than ProofGeneral that tickles this bug. As far as Isabell/PG
are concerned, it's not a new problem -- it also affects Isabelle2011. See

  http://debbugs.gnu.org/cgi/bugreport.cgi?bug=8703

(Note that I encountered this problem with Linux -- I hope that the MacOS
version uses the same code, but I have not tested this theory.)

Best regards,

Bertram
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev