[isabelle-dev] NEWS: Computations

[Florian Haftmann]

Computations generated by the code generator can be embedded
directly into ML, alongside with @{code} antiquotations, using
the following antiquotations:

  @{computation … terms: … datatypes: …} :
((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
  @{computation_conv … terms: … datatypes: …} :
(Proof.context -> 'ml -> conv) -> Proof.context -> conv
  @{computation_check terms: … datatypes: …} :
Proof.context -> conv

See src/HOL/ex/Computations.thy,
src/HOL/Decision_Procs/Commutative_Ring.thy and
src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
tutorial on code generation.



This refers to fd753468786f and is IMHO a remarkable mile stone in the
overall code generation / reflection / proof procedure business after
more than 10 years of previous unsatisfactory attempts in that area.

The details are explained in a dedicated chapter §6 of the tutorial on
code generation.

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] The Great Picard Theorem

[Lawrence Paulson]

I have just added this to the Analysis directory, making its inevitable 
refactoring more necessary.

Arguably it should be an AFP entry. Unfortunately, I’m not sufficiently expert 
in complex analysis to say whether it is core material or not. It looks like a 
fundamental result to me.

We should probably resolve the question of Analysis before the next release. 
How do we decide which things go into Complex_Main versus Analysis (which could 
be split into basic/advanced) and the AFP?

Larry

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

Re: [isabelle-dev] Bitbucket SSH craziness escalates

[Lawrence Paulson]

I shall have to file this one under “mercurial mysteries”, which is already a 
supermassive black hole.

I got the push to work, now I’m hoping I don’t have to touch it again for a 
long time.

Larry

> On 21 Feb 2017, at 21:56, Blanchette, J.C.  wrote:
> 
> 
>> On 21.02.2017, at 22:12, Lawrence Paulson > > wrote:
>> 
>> I committed some changes (fixing AFP-devel), which I would like to push. But 
>> what in God’s name is this?
>> 
>> ~/isabelle/afp/devel/thys: hg push
>> pushing to https://bitbucket.org/isa-afp/afp-devel 
>> 
> 
> In your ~/isabelle/afp/devel/.hg/hgrc, I presume there's a line that looks 
> like this:
> 
>   default = https://bitbucket.org/isa-afp/afp-devel 
> 
> 
> Change it to
> 
>   default = ssh://h...@bitbucket.org/isa-afp/afp-devel 
> 
> Jasmin
> 

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

[isabelle-dev] Build failure in slow sessions

[Lars Hupel]

Dear developers,

there have been some failures in the last two runs of the slow sessions:

https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/349/
https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/348/

(Relevant changesets are listed there.)

Unfortunately there have been no emails because for some reason, they
ran into the "hard" timeout as imposed by Jenkins. I will investigate
why they haven't been aborted the proper way.

What seems interesting are those two consecutive lines of log:

11:07:25.458 Iptables_Semantics_Examples: theory
Analyze_Synology_Diskstation
19:01:48.518 Run out of store - interrupting threads

(timestamps are elapsed time)

So, nothing happens for a while and then we get an out of memory error.
Note that the "slow" sessions are executed on 64 bit with an abundance
of memory.

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