Re: [isabelle-dev] HOL/Computational_Algebra/Polynomial.thy

[Florian Haftmann]

> Is it right for this theory to base itself on HOL.Deriv rather than 
> Complex_Main?
> 
> Larry
> 
> section ‹Polynomials as type over a ring structure›
> 
> theory Polynomial
> imports
>   HOL.Deriv
>   "HOL-Library.More_List"
>   "HOL-Library.Infinite_Set"
>   Factorial_Ring
> begin

I don't think so, especially the combination of theories from
HOL-Library with a non-canonical theory entry is weird.

I am unable to tell on the spot how this has emerged.  Are there any
suspicious things when HOL.Deriv is replaces by Complex_Main?

I guess that theory uses some analytical results and hence cannot build
on Main alone.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] HOL/Computational_Algebra/Polynomial.thy

[Lawrence Paulson]

Is it right for this theory to base itself on HOL.Deriv rather than 
Complex_Main?

Larry

section ‹Polynomials as type over a ring structure›

theory Polynomial
imports
  HOL.Deriv
  "HOL-Library.More_List"
  "HOL-Library.Infinite_Set"
  Factorial_Ring
begin

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

Re: [isabelle-dev] Isabelle build only works in certain directories

[Lawrence Paulson]

My last email was premature, because the exact same thing happened again: it 
hung at 2:15 minutes of CPU time. Fortunately I was able to kill it and retry, 
and thanks to multithreading, you don't have to wait anything like two minutes 
before reaching the two minute mark.

Larry

> On 28 Jun 2018, at 14:58, Lawrence Paulson  wrote:
> 
> I wonder whether this relates to the problem I have seen from time to time, 
> where the build process "goes to sleep" around two minutes into building HOL. 
> It's reproducible enough that I can feel confident that HOL will build only 
> when the activity monitor shows that the process has consumed at least three 
> minutes of CPU time. But I haven't seen it for a couple of weeks. 
> 
> I am (currently) running macOS High Sierra 10.13.5 but there may have been an 
> OS update during that time. It may be worth updating your system and trying 
> again.
> 
> Larry
> 
>> On 28 Jun 2018, at 12:25, Max Haslbeck  wrote:
>> 
>> 
>> I have the following curious problem: isabelle build only seems to work when 
>> I’m in certain directories.
>> 
>> Steps to reproduce:
>> 1. Start out with clean mercurial repository of isabelle in 
>> '/Users/mhaslbeck/Projects/isabelle'
>> 2. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle components -I'
>> 3. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle components -a'
>> 4. run 'cd /'
>> 5. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
>> Output:
>> ```
>> ### Building Isabelle/Scala ...
>> Started at Thu Jun 28 13:03:18 GMT+2 2018 (polyml-5.7.1_x86-darwin on 
>> lap44-cl-c703)
>> ISABELLE_BUILD_OPTIONS=""
>> 
>> ML_PLATFORM="x86-darwin"
>> ML_HOME="/Users/mhaslbeck/.isabelle/contrib/polyml-5.7.1-6/x86-darwin"
>> ML_SYSTEM="polyml-5.7.1"
>> ML_OPTIONS="--minheap 500"
>> 
>> Session Pure/Pure
>> ```
>> 6. The build process now freezes and doesn’t react to keyboard input, can be 
>> killed by 'pkill java'
>> 7. run 'mkdir ~/tmp; cd ~/tmp'
>> 8. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
>> freezes with same output as in 5.
> 

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

Re: [isabelle-dev] Isabelle build only works in certain directories

[Lawrence Paulson]

I wonder whether this relates to the problem I have seen from time to time, 
where the build process "goes to sleep" around two minutes into building HOL. 
It's reproducible enough that I can feel confident that HOL will build only 
when the activity monitor shows that the process has consumed at least three 
minutes of CPU time. But I haven't seen it for a couple of weeks. 

I am (currently) running macOS High Sierra 10.13.5 but there may have been an 
OS update during that time. It may be worth updating your system and trying 
again.

Larry

> On 28 Jun 2018, at 12:25, Max Haslbeck  wrote:
> 
> 
> I have the following curious problem: isabelle build only seems to work when 
> I’m in certain directories.
> 
> Steps to reproduce:
> 1. Start out with clean mercurial repository of isabelle in 
> '/Users/mhaslbeck/Projects/isabelle'
> 2. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle components -I'
> 3. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle components -a'
> 4. run 'cd /'
> 5. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
>  Output:
> ```
> ### Building Isabelle/Scala ...
> Started at Thu Jun 28 13:03:18 GMT+2 2018 (polyml-5.7.1_x86-darwin on 
> lap44-cl-c703)
> ISABELLE_BUILD_OPTIONS=""
> 
> ML_PLATFORM="x86-darwin"
> ML_HOME="/Users/mhaslbeck/.isabelle/contrib/polyml-5.7.1-6/x86-darwin"
> ML_SYSTEM="polyml-5.7.1"
> ML_OPTIONS="--minheap 500"
> 
> Session Pure/Pure
> ```
> 6. The build process now freezes and doesn’t react to keyboard input, can be 
> killed by 'pkill java'
> 7. run 'mkdir ~/tmp; cd ~/tmp'
> 8. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
>  freezes with same output as in 5.

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

Re: [isabelle-dev] Isabelle build only works in certain directories

[Makarius]

On 28/06/18 13:25, Max Haslbeck wrote:
> 
> I have the following curious problem: isabelle build only seems to work when 
> I’m in certain directories.
> 4. run 'cd /'
> 5. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
>   Output:
> 6. The build process now freezes and doesn’t react to keyboard input, can be 
> killed by 'pkill java'

> OS: macOS High Sierra 10.13.4
> Isabelle rev: f5ca4c2157a5

I have made some experiments with this Isabelle version and macOS
10.13.5, but did not see any such problems.

Maybe there is something odd with the local file-system setup
(encryption, "protections" by Apple etc.). It could be again some fight
of Oracle (Java) vs. Apple.


> Is there any way to get more verbose output from the building process?

Pure is the initial bootstrap: you may get more information if you build
it from a different directory first, and then repeat the experiment with
"isabelle build -b FOL".

An alternative experiment: use "isabelle scala" to build from the
running Isabelle/Scala process:

  import isabelle._

  val options = Options.init()

  Build.build(options, new Console_Progress, sessions = List("Pure"),
verbose = true)



Can you try if some older Isabelle version still works?

You can use "hg up -r Isabelle2017" (or other tags or revs) and then
repeat "isabelle components -a && isabelle jedit -bf" + build invocations.

If you have found a good situation, you can also use hg bisect to narrow
it down:

  hg bisect --reset  #once
  hg up -r f5ca4c2157a5 ; hg bisect --bad

Then "hg bisect --bad" or "hg bisect --good" to record the changing
state of that point in history.


You can also check the particular versions where the underlying JDK
changes: hg grep --all jdk Admin/components/main


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

[isabelle-dev] Isabelle build only works in certain directories

[Max Haslbeck]

Hi,

I have the following curious problem: isabelle build only seems to work when 
I’m in certain directories.

Steps to reproduce:
1. Start out with clean mercurial repository of isabelle in 
'/Users/mhaslbeck/Projects/isabelle'
2. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle components -I'
3. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle components -a'
4. run 'cd /'
5. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
  Output:
```
### Building Isabelle/Scala ...
Started at Thu Jun 28 13:03:18 GMT+2 2018 (polyml-5.7.1_x86-darwin on 
lap44-cl-c703)
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86-darwin"
ML_HOME="/Users/mhaslbeck/.isabelle/contrib/polyml-5.7.1-6/x86-darwin"
ML_SYSTEM="polyml-5.7.1"
ML_OPTIONS="--minheap 500"

Session Pure/Pure
```
6. The build process now freezes and doesn’t react to keyboard input, can be 
killed by 'pkill java'
7. run 'mkdir ~/tmp; cd ~/tmp'
8. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
  freezes with same output as in 5.
9. run 'mkdir ~/tmp/tmp; cd ~/tmp/tmp'
10. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
  build process finishes successfully

Is there any way to get more verbose output from the building process?

Specs:
OS: macOS High Sierra 10.13.4
Isabelle rev: f5ca4c2157a5

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

Re: [isabelle-dev] a question about regulations

[Makarius]

On 28/06/18 07:55, José Manuel Rodriguez Caballero wrote:
> 
>   Motivated by my exchange of experiences with professionals using
> proof-assistants like Coq for commercial purposes, I would like to ask
> the following question is: which are the regulations of Isabelle for
> commercial use? For example, if a software company is interested in
> selling .thy files to clients, which conditions apply?

(Why is this on isabelle-dev? It is not relevant to the Isabelle
development process. Isabelle theory development is a normal user activity.)

Isabelle itself is subject to the very liberal BSD-style license scheme.
Its add-on tools might have other Open Source licenses. The overall
Isabelle application taken together converges to the strictest Open
Source license of any of its components, similar to a Linux distribution.

Whatever you produce yourself with the Isabelle application is *not*
affected by any of this. You can publish your own outcome by whatever
license you like, even a non-Open-Source license.


But note that after some decades of Open Source culture, almost
everything of relevance is published Open Source now. Even if you "sell"
sources, you can often tell the one who pays for it that it is vital to
publish the results under such a reusable license: this will allow other
people in the same situation to build on it and improve the body of
available material in the next round of the universal iteration process.

Ideally it will all end up in the Archive of Formal Proofs eventually,
where it is maintained "automagically", i.e. updated to new Isabelle
versions as they emerge. This is a privilege of the participants in the
Open Source cartel.


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

[isabelle-dev] Jenkins reconfiguration

[Lars Hupel]

Dear Isabelle developers,

you may have already noticed that some Jenkins jobs got reconfigured.

The following changes are relevant for developers:

- The new job "isabelle-all" runs Isabelle+AFP together, incrementally.
This should improve overall performance and avoid double builds. There
is, once again, an automatic "grace period" of 2 minutes to allow
simultaneous Isabelle+AFP changes to be pushed before a build starts.


- The jobs "afp-repo" and "isabelle-repo" and subjobs will disappear
from the front page and the status page soon. Old links will continue to
work (i.e. historic builds will not be deleted).

- The "testboard" job will also be replaced to run Isabelle+AFP
together. Historic builds will be deleted, as they are not relevant for
the official history.

Some display changes:

Jenkins will show a failure summary on the link that is in the email
(example in the attachment).

There are more changes related to the testboard in the pipeline.

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

Re: [isabelle-dev] a question about regulations

[Gerwin.Klein]

Isabelle is distributed under a BSD 3-clause license. The only restrictions for 
Isabelle itself are (see COPYRIGHT file):

* Redistributions of source code must retain the above copyright 
notice, this list of conditions and the following disclaimer.

* Redistributions in binary form must reproduce the above copyright 
notice, this list of conditions and the following disclaimer in the 
documentation and/or other materials provided with the distribution.

* Neither the name of the University of Cambridge or the Technische
Universitaet Muenchen nor the names of their contributors may be used
to endorse or promote products derived from this software without
specific prior written permission.

This is very permissive.

There are no restrictions for other .thy files, only the usual copyright and 
other IP laws apply. We have commercial contracts that deliver .thy files quite 
routinely.

Cheers,
Gerwin

> On 28 Jun 2018, at 07:55, José Manuel Rodriguez Caballero 
>  wrote:
> 
> Dear Sir or Madam,
> 
>   Motivated by my exchange of experiences with professionals using 
> proof-assistants like Coq for commercial purposes, I would like to ask the 
> following question is: which are the regulations of Isabelle for commercial 
> use? For example, if a software company is interested in selling .thy files 
> to clients, which conditions apply?
> 
> Sincerely yours,
> José M.l Rodriguez Caballero
> Université du Québec à Montréal
> ___
> 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

[isabelle-dev] a question about regulations

[José Manuel Rodriguez Caballero]

Dear Sir or Madam,

  Motivated by my exchange of experiences with professionals using
proof-assistants like Coq for commercial purposes, I would like to ask the
following question is: which are the regulations of Isabelle for commercial
use? For example, if a software company is interested in selling .thy files
to clients, which conditions apply?

Sincerely yours,
José M.l Rodriguez Caballero
Université du Québec à Montréal
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Clarification on ISABELLE_OUTPUT env variable removal

[Rafal Kolanski]

On 28/06/18 05:27, Makarius wrote:
> On 25/06/18 06:45, Rafal Kolanski wrote:
>>
>> While looking at Isabelle 2018, we have noticed that the ISABELLE_OUTPUT
>> environment variable functionality has been removed.
> 
> This refers to
> 
> changeset:   68219:c0341c0080e2
> user:wenzelm
> date:Sat May 19 15:45:45 2018 +0200
> description:
> clarified store directories;
> discontinued settings ISABELLE_PATH, ISABELLE_OUTPUT;
> 
> 
>> A typical setting of ISABELLE_OUTPUT/ISABELLE_PATH we use here is:
>>
>> USER_HEAPS=${OVERRIDE_USER_HEAPS:-"$ISABELLE_HOME_USER/heaps-${L4V_ARCH}${ISABELLE_HOME//\//-}"}
>> ISABELLE_OUTPUT=${OVERRIDE_ISABELLE_OUTPUT:-"$USER_HEAPS"}
>> ISABELLE_PATH=${OVERRIDE_ISABELLE_PATH:-"$USER_HEAPS"}
> 
> This example already motivates the change: ISABELLE_OUTPUT and
> ISABELLE_PATH were somehow duplicates, with subtle differences. Together
> with the "system build mode" (option -s of "isabelle build", "isabelle
> jedit" etc.) it has lead to an ill-defined situation.

Agreed, ISABELLE_PATH and ISABELLE_OUTPUT were confusing.

> I have now refined the change further in
> 
> changeset:   68523:ccacc84e0251
> user:wenzelm
> date:Wed Jun 27 20:31:22 2018 +0200
> description:
> clarified settings -- avoid hard-wired directories;
> tuned documentation;
> 
> 
> I.e. you can use ISABELLE_HEAPS above.

My sincere thanks for adding this, it really makes a big difference to
our workflow.

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