[isabelle-dev] Update of Haskell Stack

2018-12-28 Thread Makarius
Here are some notable changes concerning the Haskell Stack, which is a
build tool with a package repository behind it:

changeset:   69526:5574d504cf36
tag: tip
user:wenzelm
date:Fri Dec 28 19:01:35 2018 +0100
files:   etc/settings
description:
more conservative update of Haskell stack (amending 04e54f57a869): 13.0
still lacks notable packages like "Agda" or "darcs";


changeset:   69512:04e54f57a869
parent:  69506:7d59af98af29
user:Lars Hupel 
date:Thu Dec 27 17:36:19 2018 +0100
files:   etc/settings src/Pure/General/path.ML
description:
update LTS Haskell version


I am myself still in the process of learning how the Stack community and
release process works. Spending 5 min with the announcement of lts-13.0
from Isabelle/04e54f57a869 leaves the impression that a new major
release is merely the factual start for package maintainers to become
serious about updating and publishing their stuff.

Haskell Stack LTS versions should appear every 3-6 months -- according
to the official statement
https://github.com/commercialhaskell/lts-haskell#readme

So it looks like it is better to stay one major release version behind
the frontier of ongoing LTS development. Moreover, I have so far
refrained from updating minor versions without particular reasons: it
always causes a lot of network traffic and disk usage increase for local
.stack directories.


Here is also a concrete project that refers to Isabelle/Haskell from
isabelle-dev and is in sync with its Stack version:


https://github.com/Naproche/Naproche-SAD/commit/2af938e09a61c14f57af40679bb340a92b521331

This proves the use and usability of the emerging Isabelle/Haskell
infrastructure. In the longer term it might help more users out there to
develop Haskell-based projects for Isabelle; or just use other ITP
systems like Agda -- when OPAM gets into better shape we could also
apply this principle to Coq.


Overall, the general approach of the Isabelle distribution is to deliver
canonical versions of add-on tools that just work without manual tinkering.

Thus "latest" things require more than one close look before adopting them.


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


Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?

2018-12-28 Thread Lawrence Paulson
Tons of useful stuff here.

Some syntactic ambiguities, particularly around the =o relation, which is also 
defined as Set_Algebras.elt_set_eq.

I don’t suppose there’s any chance of using quotients to define actual 
cardinals and use ordinary equality? And it still makes sense to introduce the 
actual notion of equipollence and similar relations.

Larry

> On 27 Dec 2018, at 20:29, Makarius  wrote:
> 
> On 27/12/2018 17:45, Traytel  Dmitriy wrote:
>> Hi Larry,
>> 
>> the HOL-Cardinals library might be just right for the purpose:
>> 
>> theory Scratch
>>  imports "HOL-Cardinals.Cardinals"
>> begin
>> 
>> lemma "|A| ≤o |B| ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)"
>>  by (rule card_of_ordLeq[symmetric])
>> 
>> lemma "|A| =o |B| ⟷ (∃f. bij_betw f A B)"
>>  by (rule card_of_ordIso[symmetric])
>> 
>> lemma
>>  assumes "|A| ≤o |B|" "|B| ≤o |A|"
>>  shows "|A| =o |B|"
>>  by (simp only: assms ordIso_iff_ordLeq)
>> 
>> end
>> 
>> The canonical entry point for the library is the above 
>> HOL-Cardinals.Cardinals. Many of the theorems and definitions are already in 
>> Main, because the (co)datatype package is based on them. The syntax is 
>> hidden in main—one gets it by importing HOL-Library.Cardinal_Notations 
>> (which HOL-Cardinals.Cardinals does transitively).
> 
> It would be great to see this all consolidated and somehow unified, i.e.
> some standard notation in Main as proposed by Larry (potentially as
> bundles as proposed by Florian), and avoidance of too much no_syntax
> remove non-standard notation from Main.
> 
> 
>   Makarius

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