> 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
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
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,
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
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
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
>
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
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
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
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
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
11 matches
Mail list logo
