Re: [isabelle-dev] infix line breaking

2019-02-23 Thread Lawrence Paulson
I’d be in favour!
Larry

> On 23 Feb 2019, at 15:07, Makarius  wrote:
> 
> It might be better to introduce a proof-local version of 'abbreviation'.

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


Re: [isabelle-dev] Towards Poly/ML 5.8

2019-02-23 Thread Makarius
On 23/02/2019 11:45, Lars Hupel wrote:
>> After a lot of refinements by David Matthews we are moving towards the
>> new Poly/ML 5.8 release. Isabelle/8c587dd44f51 already bundles a Poly/ML
>> version of that number, without being official yet. The Isabelle NEWS
>> already talk about an official release:
> 
> Is it intentional that the system identifier is still 5.7.1?
> 
>   ML_SYSTEM=polyml-5.7.1
> 
> This also raises the question if that variable has any remaining uses.

In 8c587dd44f51, I made some changes on two machines, but did not copy
everything to the target, thus the etc/settings of the component is
lagging behind.

Right now ML_SYSTEM happens to have no meaning apart from some comment
about the approximative version being used. Over the years it was
sometimes used in conditional compilation and may get used like that at
some point.

Even ML_OPTIONS is less important these days that some years ago,
because Isabelle/Scala provides most of the environment to the poly process.


I did not change anything here, because build_history and the
build_status database record the Poly/ML settings over many years, and I
did not want to break the persistent data model just to be fully
up-to-date at the "tip" version.


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


Re: [isabelle-dev] infix line breaking

2019-02-23 Thread Makarius
On 23/02/2019 12:25, Lawrence Paulson wrote:
> Which reminds me: I define such abbreviations all the time, using “let”. 
> Could let-abbreviations be folded upon printing?
> 
>> On 23 Feb 2019, at 09:10, Manuel Eberl  wrote:
>>
>> I for one almost always do
>>
>>   define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})"

It might be better to introduce a proof-local version of 'abbreviation'.


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


Re: [isabelle-dev] infix line breaking

2019-02-23 Thread Lawrence Paulson
Which reminds me: I define such abbreviations all the time, using “let”. Could 
let-abbreviations be folded upon printing?

Larry

> On 23 Feb 2019, at 09:10, Manuel Eberl  wrote:
> 
> I for one almost always do
> 
>   define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})"
> 
> in such cases, perhaps occasionally combined with a
> 
>   note [simp] = G_def [symmetric]
> 
> at least during the "exploratory" stage of Isar proof writing.
> 
> Without that, statements and proof obligations in HOL-Algebra become
> totally unreadable in my experience.
> 
> Manuel
> 
> 
> On 22/02/2019 17:20, Lawrence Paulson wrote:
>> The pretty printing of infix operators looks pretty terrible in the presence 
>> of large terms.
>> 
>> I’d like to propose having infix operators breaking at the start of the line 
>> rather than at the end. Any thoughts?
>> 
>> Larry
>> 
>> inv⇘homology_group 0 (nsphere 0)⇙ hom_induced 0 (subtopology (nsphere 0) 
>> {pp}) {} (nsphere 0) {} r
>>   d =
>>hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id
>> (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 
>> 0) {nn}) {} r
>>   (inv⇘homology_group 0 (subtopology (nsphere 0) {pp})⇙ d))
>> ___
>> 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 mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Towards Poly/ML 5.8

2019-02-23 Thread Lars Hupel

After a lot of refinements by David Matthews we are moving towards the
new Poly/ML 5.8 release. Isabelle/8c587dd44f51 already bundles a 
Poly/ML

version of that number, without being official yet. The Isabelle NEWS
already talk about an official release:


Is it intentional that the system identifier is still 5.7.1?

  ML_SYSTEM=polyml-5.7.1

This also raises the question if that variable has any remaining uses.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] infix line breaking

2019-02-23 Thread Manuel Eberl
I for one almost always do

  define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})"

in such cases, perhaps occasionally combined with a

  note [simp] = G_def [symmetric]

at least during the "exploratory" stage of Isar proof writing.

Without that, statements and proof obligations in HOL-Algebra become
totally unreadable in my experience.

Manuel


On 22/02/2019 17:20, Lawrence Paulson wrote:
> The pretty printing of infix operators looks pretty terrible in the presence 
> of large terms.
>
> I’d like to propose having infix operators breaking at the start of the line 
> rather than at the end. Any thoughts?
>
> Larry
>
> inv⇘homology_group 0 (nsphere 0)⇙ hom_induced 0 (subtopology (nsphere 0) 
> {pp}) {} (nsphere 0) {} r
>d =
> hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id
>  (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 
> 0) {nn}) {} r
>(inv⇘homology_group 0 (subtopology (nsphere 0) {pp})⇙ d))
> ___
> 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