Re: [isabelle-dev] Use HTTPS for components

[Gerwin Klein]

I agree, we should do that.

Ideally, we should actually sign those components. The 
downloading/receiving/checking side is not too hard to automate, but it would 
require entering the private key keyphrase when you are signing (providing) a 
new component.

Cheers,
Gerwin

> On 13 Jul 2016, at 08:28, Lars Hupel  wrote:
>
> Dear Isabelle developers,
>
> all of the critical Isabelle infrastructure (even website mirrors) is
> reachable via HTTPS. For Jenkins, it's not so important. For executable
> code, it is very important. Hence I would like to propose a simple
> change in the global "etc/settings":
>
> -ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components";
> +ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components";
>
> Because we don't sign components, we should at least make them available
> over HTTPS. This is the bare minimum according to security best practices.
>
> Potential disadvantage: Fetching from HTTPS using Perl's libwww requires
> an addon package ("LWP-Protocol-https").
>
> Potential remedy: Switch to curl for fetching components
> - readily available everywhere
> - less Perl required
>
> (Note that it appears that that specific Perl addon is not available
> under Cygwin.)
>
> I don't think we should let shortcomings of some Perl module dictate a
> lack of security.
>
> Cheers
> Lars
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Use HTTPS for components

[Lars Hupel]

Dear Isabelle developers,

all of the critical Isabelle infrastructure (even website mirrors) is
reachable via HTTPS. For Jenkins, it's not so important. For executable
code, it is very important. Hence I would like to propose a simple
change in the global "etc/settings":

-ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components";
+ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components";

Because we don't sign components, we should at least make them available
over HTTPS. This is the bare minimum according to security best practices.

Potential disadvantage: Fetching from HTTPS using Perl's libwww requires
an addon package ("LWP-Protocol-https").

Potential remedy: Switch to curl for fetching components
- readily available everywhere
- less Perl required

(Note that it appears that that specific Perl addon is not available
under Cygwin.)

I don't think we should let shortcomings of some Perl module dictate a
lack of security.

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

[isabelle-dev] NEWS: refined folding mode "isabelle"

[Makarius]

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

* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
are treated as delimiters for fold structure.


This refers to Isabelle/f10feaa9b14a.


Makarius

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

Re: [isabelle-dev] NEWS: Indentation according to Isabelle outer syntax

[Makarius]

This is the updated situation according to Isabelle/019856db2bb6:

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

* Improved support for indentation according to Isabelle outer syntax.
Action "indent-lines" (shortcut C+i) indents the current line according
to command keywords and some command substructure. Action
"isabelle.newline" (shortcut ENTER) indents the old and the new line
according to command keywords only; see also option
"jedit_indent_newline".


As usual, new keyboard shortcuts are only applied automatically for
fresh Isabelle/jEdit installations. To benefit from isabelle.newline it
needs to be added manually in the Global Options / Shortcuts dialog.

With a little bit of practice, it already works quite smoothly and
requires very few additional C+i, TAB, S+TAB etc.


Makarius

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

Re: [isabelle-dev] Simplification theorems with more general typeclasses

[Mathias Fleury]

For the record, I have now pushed the change to Isabelle, see 
http://isabelle.in.tum.de/reports/Isabelle/rev/3365c8ec67bd 
.

Mathias

> On 05 Jul 2016, at 14:03, Mathias Fleury  wrote:
> 
> Hi all,
> 
> after some more experiments, I found out that there is another difference 
> between explicit typeclass annotations and lemmas in the context: the former 
> theorems are included in instantiations but are not included in 
> interpretations. This usually does not make a difference, since there is 
> usually a single order on a type.
> 
> Instead, I introduced an additional typeclass to the hierarchy. The change 
> was successfully tested on testboard (mercurial diff 
> , status 
> ), and does not need 
> any AFP change.
> 
> 
> Does someone have an opinion on this change?
> 
> 
> Mathias
>  
>> On 04 Jul 2016, at 14:20, Mathias Fleury > > wrote:
>> 
>> Hi Johannes,
>> 
>> 
>> the multiset ordering (contrary to the subset ordering) does not have this 
>> property:
>> 
>>  lemma "{#0#} <= {#Suc 0#}”
>>unfolding Multiset_Order.le_multiset⇩H⇩O by auto
>> 
>> (the actual notation is #⊆# and not <=).
>> 
>> 
>> I tried locally to apply the changes of my previous email this week-end. 
>> Except some proofs inside the typeclass definitions (i.e. in the files 
>> Groups.thy, Rings.thy, and Missing_Ring.thy), no other changes were needed 
>> in Isabelle or the AFP.
>> 
>> 
>> Thanks for your answer,
>> Mathias
>> 
>> 
>>> On 04 Jul 2016, at 13:22, Johannes Hölzl >> > wrote:
>>> 
>>> Hi Mathias,
>>> 
>>> there is at least the type class 'canonically_ordered_monoid' which has
>>> the property a <= b <--> ?c. a + c = b which implies 0 <= a for all a.
>>> Are the multisets already in this typeclass?
>>> 
>>>  - Johannes
>>> 
>>> 
>>> Am Dienstag, den 28.06.2016, 10:04 +0100 schrieb Mathias Fleury:
 Dear type-classes and simplifier experts,
 
 in the plan of instantiating multisets with the multiset ordering, I
 am trying to instantiate the multisets with additional typeclasses to
 get specific simplification theorems. The aim is to mimic the
 simplifier’s behaviour of other types like natural numbers. One of my
 problems can be nicely illustrated by the following lemma: “M <= M +
 N <-> 0 <= N”. 
 
 
 Analog simplification rules already exist for rings (e.g., natural
 numbers*) and ordered groups too:
thm
 Rings.linordered_semiring_class.less_eq_add_cancel_left_greater_eq_ze
 ro
thm Groups.ordered_ab_group_add_class.le_add_same_cancel1
 Both rules are stating that “M <= M + N <—> 0 <= N” and are marked as
 [simp].
 
 
 However, the multisets are neither a group (no inverse for the law
 “+”) nor a ring (no multiplication). I could duplicate the theorems,
 but I noticed that the proofs of the theorems do only rely on the
 fact it is a monoid_add (for the zero element) and an
 ordered_ab_semigroup_add_imp_le (for the order). The following
 theorem would work too and is general enough to include the multiset
 case:
 
 lemma le_add_same_cancel1 [simp]:
   “(a :: 'a :: {monoid_add, ordered_ab_semigroup_add_imp_le}) ≤ a + b
 ⟷ 0 ≤ b”
   using add_le_cancel_left [of a 0] by simp
 
 
 Are there any obvious differences between this more general version
 with explicit type class annotations
 and Groups.ordered_ab_group_add_class.le_add_same_cancel1? If no,
 would it make sense to use this version in Isabelle?
 
 
 
 Thanks in advance,
 Mathias Fleury
 
 
 
 
 * for natural numbers, the simproc
 Numeral_Simprocs.natle_cancel_numerals is able to do it too.
 ___
 isabelle-dev mailing list
 isabelle-...@in.tum.de 
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel 
 
 le-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
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

__