[isabelle-dev] NEWS: theorem eigen context

[Makarius]

*** Isar ***

* Toplevel theorem statements support eigen-context notation with 'if' /
'for' (in postix), which corresponds to 'assumes' / 'fixes' in the
traditional long statement form (in prefix). Local premises are called
"that" or "assms", respectively. Empty premises are *not* bound in the
context: INCOMPATIBILITY.


This refers to to Isabelle/056ea294c256. The 'if' / 'for' notation is
often more convenient, and fits to the same notation for Isar proof
language elements: 'assume', 'have', 'show' etc.

Long theorem statements with 'fixes' / 'assumes' and 'shows' / 'obtains'
are not going away. This form also supports 'includes' and 'defines'.
(The latter is a bit odd in many respects, but cannot be discontinued
realistically.)


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

[isabelle-dev] NEWS: cartouches

[Makarius]

*** General ***

* Embedded content (e.g. the inner syntax of types, terms, props) may be
delimited uniformly via cartouches. This works better than old-fashioned
quotes when sub-languages are nested.


*** Prover IDE -- Isabelle/Scala/jEdit ***

* Cartouche abbreviations work both for " and ` to accomodate typical
situations where old ASCII notation may be updated.


This refers e.g. to Isabelle/4cf6726eb85e, which also contains more
unification of "embedded" language tokens: type, term, prop, text. Thus
the complexity of Isabelle language nesting is reduced, thanks to more
uniform notation.


When demonstrating Isabelle occasionally to people who have never seen
it before, there is often a spontaneous puzzlement about ASCII quotes
around inner syntax. With cartouches that surprise might be avoided,
since it is not associated with already known syntax.

Still missing: a tool for systematic replacement of such semantic
cartouches. Purely syntactic ones are already handled by "isabelle
update_cartouches".


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

Re: [isabelle-dev] pretty-printing of DIM('a)

[Makarius]

On 03/04/16 14:50, Lawrence Paulson wrote:
> The DIM('a) notation is introduced in Multivariate_Analysis/Euclidean_Space, 
> for referring to the dimension of the Euclidean space designated by type ‘a. 
> (See code snippet below.) Unfortunately, DIM(‘a) pretty-prints as card Basis, 
> and the type reference is lost.

This was accidentally broken in 2012. See now:

changeset:   63128:7e5084ad95aa
user:wenzelm
date:Tue May 24 17:51:09 2016 +0200
files:   src/HOL/Multivariate_Analysis/Euclidean_Space.thy
description:
recovered printing of DIM('a) (cf. 899c9c4e4a4c);


Makarius

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

Re: [isabelle-dev] NEWS: process management (summary and update)

[Makarius]

On 20/03/16 06:41, Lars Noschinski wrote:
> On 11.03.2016 18:37, Makarius wrote:
>> * The executable "isabelle_process" has been discontinued. Tools and
>> prover front-ends should use ML_Process or Isabelle_Process in
>> Isabelle/Scala. INCOMPATIBILITY.
>>
>> * New command-line tool "isabelle process" supports ML evaluation of
>> literal expressions (option -e) or files (option -f) in the context of a
>> given heap image. Errors lead to premature exit of the ML process with
>> return code 1.
> 
> To whomever is now maintaining Haskabelle (Ondřej?): This change breaks
> Haskabelle as it calls isabelle_process to build its adaptation table
> (in lib/mk_adapt).

This seems to be still open.

Is there a remaining maintainer of Haskabelle?


Makarius


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

Re: [isabelle-dev] Isabelle repository broken

[Manuel Eberl]

Argh! You are correct. Today is /not/ my day. I'm on it.


On 24/05/16 18:42, Makarius wrote:

On 24/05/16 18:34, Manuel Eberl wrote:

I'm confident that I'll have everyting up and running again soon.

BTW, current Isabelle/8230358fab88 now looks like too much has been
committed.


Makarius

___
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] Isabelle repository broken

[Makarius]

On 24/05/16 18:34, Manuel Eberl wrote:
> I'm confident that I'll have everyting up and running again soon.

BTW, current Isabelle/8230358fab88 now looks like too much has been
committed.


Makarius

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

Re: [isabelle-dev] Isabelle repository broken

[Manuel Eberl]

Yes, this was my fault. The problem was that I stupidly forgot to commit 
my changes before I pushed to the testboard and thus did not see the 
problems caused by my changes.


I'm confident that I'll have everyting up and running again soon.

Manuel


On 24/05/16 17:22, Jasmin Blanchette wrote:

On 24.05.2016, at 17:12, Makarius  wrote:

The Isabelle repository is broken at 76cb6c6bd7b8 (paulson) or
6a17bcddd6c2 (eberlm).

The failure is as follows:
### theory "Generate_Binary_Nat"
### 197.201s elapsed time, 259.420s cpu time, 8.924s GC time
*** "List.coset" is not a constructor, on left hand side of equation, in
theorem:
*** permutations_of_set (List.coset ?xs) \
...

Looking at the history, it's hard to believe the culprit would be anything but 
change dd651e3f7413.

Jasmin

___
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] Isabelle repository broken

[Jasmin Blanchette]

On 24.05.2016, at 17:12, Makarius  wrote:
> 
> The Isabelle repository is broken at 76cb6c6bd7b8 (paulson) or
> 6a17bcddd6c2 (eberlm).
> 
> The failure is as follows:
> ### theory "Generate_Binary_Nat"
> ### 197.201s elapsed time, 259.420s cpu time, 8.924s GC time
> *** "List.coset" is not a constructor, on left hand side of equation, in
> theorem:
> *** permutations_of_set (List.coset ?xs) \
> ...

Looking at the history, it's hard to believe the culprit would be anything but 
change dd651e3f7413.

Jasmin

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

Re: [isabelle-dev] Isabelle repository broken

[Lars Hupel]

> https://ci.isabelle.systems/jenkins shows many dark clouds and
> thunderbolts, but I have no clue where to look precisely.

Jenkins is a complex piece of software (much more complex than
Isabelle), so it is indeed hard to figure out where to click.

The best way to stay on top of the current state is to subscribe to the
[isabelle-ci] mailing list:

  

In case of failure in either the Isabelle distribution or the
development AFP, there will be a mail including the build log. I have
attached the latest mail here.

> In principle, such a situation cannot happen: everybody knows that
> pushes to the Isabelle repository require a full test that is equivalent
> to "isabelle build -a".

Let me also point out the existence of the testboards again:

  
  

They are fully functional.

Cheers
Lars


PS: The weather icons appear reflect the current weather in Munich :-)
--- Begin Message ---
The Isabelle build failed. See the log at: 
https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/197/

build.log
Description: Binary data
___
Isabelle-ci mailing list
isabelle...@mail46.informatik.tu-muenchen.de
https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci
--- End Message ---
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle repository broken

[Lawrence Paulson]

I did run a full test of my changes, which in any event don’t look connected 
with the error message you report.
Larry

> On 24 May 2016, at 16:12, Makarius  wrote:
> 
> The Isabelle repository is broken at 76cb6c6bd7b8 (paulson) or
> 6a17bcddd6c2 (eberlm).
> 
> The failure is as follows:
> ### theory "Generate_Binary_Nat"
> ### 197.201s elapsed time, 259.420s cpu time, 8.924s GC time
> *** "List.coset" is not a constructor, on left hand side of equation, in
> theorem:
> *** permutations_of_set (List.coset ?xs) \
> *** Code.abort (STR ''Permutation of set complement not supported'')
> ***  (\_. permutations_of_set (List.coset ?xs))
> *** At command "export_code" (line 83 of
> "~~/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy")
> 
> 
> https://ci.isabelle.systems/jenkins shows many dark clouds and
> thunderbolts, but I have no clue where to look precisely.
> 
> 
> In principle, such a situation cannot happen: everybody knows that
> pushes to the Isabelle repository require a full test that is equivalent
> to "isabelle build -a".
> 
> 
>   Makarius
> ___
> 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] Isabelle repository broken

[Makarius]

The Isabelle repository is broken at 76cb6c6bd7b8 (paulson) or
6a17bcddd6c2 (eberlm).

The failure is as follows:
### theory "Generate_Binary_Nat"
### 197.201s elapsed time, 259.420s cpu time, 8.924s GC time
*** "List.coset" is not a constructor, on left hand side of equation, in
theorem:
*** permutations_of_set (List.coset ?xs) \
*** Code.abort (STR ''Permutation of set complement not supported'')
***  (\_. permutations_of_set (List.coset ?xs))
*** At command "export_code" (line 83 of
"~~/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy")


https://ci.isabelle.systems/jenkins shows many dark clouds and
thunderbolts, but I have no clue where to look precisely.


In principle, such a situation cannot happen: everybody knows that
pushes to the Isabelle repository require a full test that is equivalent
to "isabelle build -a".


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