[isabelle] A question about contributing to HOL

[mailing-list anonymous]

Dear All,

I would like to understand if it would be feasible for me to propose my own
contributions to HOL. I have read the section "Publish contributions as an
external" on the Isabelle community wiki (
https://isabelle.in.tum.de/community/Publish_contributions_as_an_external).
I am also aware of the mailing list isabelle-***@in.tum.de. However, this
is a general question about the possibility of a contribution being
considered, given certain specific circumstances. Thus, I believe that it
may be more useful to this mailing list, rather than isabelle-***@in.tum.de.
Otherwise, of course, please suggest to forward it to isabelle-***@in.tum.de
.

My primary concern is that I am not affiliated with an academic group or a
company that works with Isabelle/HOL on a regular basis. I have an
impression that all of the existing contributions to HOL were made by
people who are, somehow, officially affiliated with the Isabelle community.
Thus, I would like to assess whether or not my contributions would be
considered on this basis. Of course, I am also aware of the existence of
the AFP. However, I believe, some of the theorems that I would like to
propose naturally extend some of the theories that are already available in
HOL and, most likely, are not suitable to be published as an independent
AFP library.

To be more specific, I would like to provide several examples of the
contributions that I would like to propose. At the moment, HOL-Algebra
contains the theory IntRing.thy that contains the lemmas "ZFact_zero:
"carrier (ZFact 0) = (⋃a. {{a}})"" and "ZFact_one: "carrier (ZFact 1) =
{UNIV}"". However, it does not seem to contain a lemma that could describe
the carrier of a more general quotient ring "ZFact (m::int)" (e.g. "0 < m
⟹ carrier (ZFact m) = {X. ∃n ∈ {0..<m}. X = {x. m dvd (x - n)}}"). Also, I
was not able to find a relatively standard textbook theorem that
characterises a cyclic group in terms of the quotient group "add_monoid
(ZFact m)" (e.g. "finite (carrier G) ⟹ order G = m ⟹ ∃a ∈ carrier G.
carrier G = {a[^]i | i::int. i ∈ UNIV} ⟹ add_monoid (ZFact m) ≅ G"). Some
of the potential contributions are not independent theorems, but minor
extensions of the existing lemmas in "HOL", e.g. lemma "ord_dvd_pow_eq_1"
in "Algebra-Multiplicative_Group" shows that "finite (carrier G)", "a ∈
carrier G" and "a [^] k = 𝟭" together imply "ord a dvd k", where "k" is of
the type "nat". However, this lemma holds even if "k" is any number of the
type "int" (the existing proof would need to be amended to take into
account the negative values of k).

Thank you

(I would prefer not to disclose my contact details publicly for the reasons
of privacy and as a measure against spam)

[José Manuel Rodriguez Caballero]

Post by mailing-list anonymous
I would like to understand if it would be feasible for me to propose my own
contributions to HOL.

If some of your results are related to number theory, you could include
your contributions in my project of a library "number theory miscellany".
Here is my repository :
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory

But, you should include in the file either your name or a pseudonym, in
order to distinguish your contributions from my contributions. Maybe you
prefer your own miscellany, e.g., "general miscellany", "topology
miscellany", etc. In my case, my main motivation to contribute, beside the
pleasure of proving some truth, is to increase my CV, because some
reviewers of important journals, e.g., American Mathematical Monthly, said
to me that my proofs are too long to be checked and that they are annoying
for the readers (someone is confusing mathematics with comic strips). I am
successfully proving the theorems from my Master Memoir in Isabelle one by
one (work-in-progress). My first version is rather non-algorithmic, but I
have the project to include an algorithmic version in order to do explicit
computations.

Post by mailing-list anonymous
My primary concern is that I am not affiliated with an academic group or a
company that works with Isabelle/HOL on a regular basis. I have an
impression that all of the existing contributions to HOL were made by
people who are, somehow, officially affiliated with the Isabelle community.

Me neither, nevertheless, the Isabelle community, at least in my case, was
the most open research community that I have ever met. Other research
communities, like the communities of pure mathematics, are rather closed
and mathematicians in general do not read the works of outsiders (they have
not time for that), e.g., the old Gauss did not read the work of the young
Abel, because he assumed that it was wrong, the old Cauchy did not read the
work of the young Galois, etc. Proof assistants are the key for an outsider
to become an insider, because the computer guarantee that the result is
fine, even if the proof is very complex. Nevertheless, I advice you to
become part of something and to change when you will be ready: the academic
growth is step by step.

Kind Regards,
José M.

[Paulo Emílio de Vilhena]

Hello,

I’m not answering your question, but since you are working on HOL-Algebra I
would like to point out a github repository where we propose not only to
extend this library with new theories but also to revise old ones. For
instance, we already have one of the mentioned theorems you were looking
for: it is the lemma mod_ring from the theory Int_Ring (note the underline)
stated as

lemma (in int_ring) mod_ring:

assumes "a ∈ carrier R - { 𝟬 }"

shows "carrier (R Quot (PIdl a)) = (λi. PIdl a +> ⟦ i ⟧) ` {0..< ¦
int_repr a ¦}"

It’s overly complicated for now, because it’s stated for all rings
isomorphic to the ring of integers, but you can easily instantiate it for
Z. We also have a theory called Multiplicative_Group_Revised where I
started an analogous development of Multiplicative_Group but more concise
since it reuses previous developments from cycles and permutations.

Other than that, there are theories on algebraic numbers, field extensions
and division of polynomials. Our most impressive result is the existence of
the algebraic closure of a field. Here is the link for the repository in
case you want to check it out: https://github.com/DeVilhena-Paulo/GaloisCVC4

Thanks,

Paulo.


Message: 5

Date: Sat, 20 Oct 2018 15:05:07 +0300
Subject: [isabelle] A question about contributing to HOL
<
Content-Type: text/plain; charset="UTF-8"
Dear All,
I would like to understand if it would be feasible for me to propose my own
contributions to HOL. I have read the section "Publish contributions as an
external" on the Isabelle community wiki (
https://isabelle.in.tum.de/community/Publish_contributions_as_an_external
).
is a general question about the possibility of a contribution being
considered, given certain specific circumstances. Thus, I believe that it
may be more useful to this mailing list, rather than
Otherwise, of course, please suggest to forward it to
.
My primary concern is that I am not affiliated with an academic group or a
company that works with Isabelle/HOL on a regular basis. I have an
impression that all of the existing contributions to HOL were made by
people who are, somehow, officially affiliated with the Isabelle community.
Thus, I would like to assess whether or not my contributions would be
considered on this basis. Of course, I am also aware of the existence of
the AFP. However, I believe, some of the theorems that I would like to
propose naturally extend some of the theories that are already available in
HOL and, most likely, are not suitable to be published as an independent
AFP library.
To be more specific, I would like to provide several examples of the
contributions that I would like to propose. At the moment, HOL-Algebra
"carrier (ZFact 0) = (⋃a. {{a}})"" and "ZFact_one: "carrier (ZFact 1) =
{UNIV}"". However, it does not seem to contain a lemma that could describe
the carrier of a more general quotient ring "ZFact (m::int)" (e.g. "0 < m
⟹ carrier (ZFact m) = {X. ∃n ∈ {0..<m}. X = {x. m dvd (x - n)}}"). Also, I
was not able to find a relatively standard textbook theorem that
characterises a cyclic group in terms of the quotient group "add_monoid
(ZFact m)" (e.g. "finite (carrier G) ⟹ order G = m ⟹ ∃a ∈ carrier G.
carrier G = {a[^]i | i::int. i ∈ UNIV} ⟹ add_monoid (ZFact m) ≅ G"). Some
of the potential contributions are not independent theorems, but minor
extensions of the existing lemmas in "HOL", e.g. lemma "ord_dvd_pow_eq_1"
in "Algebra-Multiplicative_Group" shows that "finite (carrier G)", "a ∈
carrier G" and "a [^] k = 𝟭" together imply "ord a dvd k", where "k" is of
the type "nat". However, this lemma holds even if "k" is any number of the
type "int" (the existing proof would need to be amended to take into
account the negative values of k).
Thank you
(I would prefer not to disclose my contact details publicly for the reasons
of privacy and as a measure against spam)
End of Cl-isabelle-users Digest, Vol 160, Issue 12
**************************************************

[Tobias Nipkow]

You do not have to be affiliated with anybody to contribute to Isabelle/HOL
theories but there is no well-established process for contributing. For small
amendments you can either send them to this mailing list or contact individuals,
like the web page says that you found.

Larger contributions require more interaction with people who feel responsible
for some area. In the case of Algebra, Paulo has already indicated that there
are parellel developments that you may be able to liaise with.

Tobias

Post by mailing-list anonymous
Dear All,
I would like to understand if it would be feasible for me to propose my own
contributions to HOL. I have read the section "Publish contributions as an
external" on the Isabelle community wiki (
https://isabelle.in.tum.de/community/Publish_contributions_as_an_external).
is a general question about the possibility of a contribution being
considered, given certain specific circumstances. Thus, I believe that it
.
My primary concern is that I am not affiliated with an academic group or a
company that works with Isabelle/HOL on a regular basis. I have an
impression that all of the existing contributions to HOL were made by
people who are, somehow, officially affiliated with the Isabelle community.
Thus, I would like to assess whether or not my contributions would be
considered on this basis. Of course, I am also aware of the existence of
the AFP. However, I believe, some of the theorems that I would like to
propose naturally extend some of the theories that are already available in
HOL and, most likely, are not suitable to be published as an independent
AFP library.
To be more specific, I would like to provide several examples of the
contributions that I would like to propose. At the moment, HOL-Algebra
"carrier (ZFact 0) = (⋃a. {{a}})"" and "ZFact_one: "carrier (ZFact 1) =
{UNIV}"". However, it does not seem to contain a lemma that could describe
the carrier of a more general quotient ring "ZFact (m::int)" (e.g. "0 < m
⟹ carrier (ZFact m) = {X. ∃n ∈ {0..<m}. X = {x. m dvd (x - n)}}"). Also, I
was not able to find a relatively standard textbook theorem that
characterises a cyclic group in terms of the quotient group "add_monoid
(ZFact m)" (e.g. "finite (carrier G) ⟹ order G = m ⟹ ∃a ∈ carrier G.
carrier G = {a[^]i | i::int. i ∈ UNIV} ⟹ add_monoid (ZFact m) ≅ G"). Some
of the potential contributions are not independent theorems, but minor
extensions of the existing lemmas in "HOL", e.g. lemma "ord_dvd_pow_eq_1"
in "Algebra-Multiplicative_Group" shows that "finite (carrier G)", "a ∈
carrier G" and "a [^] k = 𝟭" together imply "ord a dvd k", where "k" is of
the type "nat". However, this lemma holds even if "k" is any number of the
type "int" (the existing proof would need to be amended to take into
account the negative values of k).
Thank you
(I would prefer not to disclose my contact details publicly for the reasons
of privacy and as a measure against spam)

[mailing-list anonymous]

Dear All,

In what follows, I address everyone who replied to my email (not in any
particular order).


To Tobias Nipkow,

Thank you for your reply. I am glad that it is potentially possible for me
to make contributions to HOL. However, of course, given that potentially
anyone can make a contribution, it would be nice if there was a
well-established process for making contributions.


To Paulo Emílio de Vilhena,

Thank you for your response and for providing the link to the repository
GaloisCVC4. I have several questions about the repository:

1. I would like to confirm that, while the main purpose of the project
GaloisCVC4 is the development of Galois Theory in the context of
HOL-Algebra, you are also making changes to HOL-Algebra that are not
directly related to the main line of the development of the project
GaloisCVC4, i.e. you may consider adding to the repository any established
results from algebra or making minor amendments/extensions of the existing
theorems that do not contribute to the main line of the development.

2. Furthermore, I would like to understand if your intention is to
integrate GaloisCVC4 with HOL-Algebra or publish it in the context of the
AFP.

3. Also, I would like to understand if you intend to discontinue the work
on the project after a certain deadline or after you achieve certain
milestones.

4. If my understanding of the dual purpose (see clause 1) of the project
GaloisCVC4 is correct, would you, potentially, accept pull requests from
external contributors?

Also, thank you for pointing out the existence of the (Isabelle)
generalisation of the proof of the characterisation of the carrier of Z/mZ.
I only wish I knew about the existence of GaloisCVC4 earlier.


To José Manuel Rodriguez Caballero,

Thank you for your reply and for providing the link to your repository. It
is good to know about the existence of this repository because it seems
that there is no mention of it in the AFP at the moment (although I cannot
be entirely certain). The lemmas that I have mentioned in my question may
fit within the context of the repository. However, they are also very
closely related to the existing Isabelle theories within HOL-Algebra, as
confirmed by Paulo Emílio de Vilhena, who has already proven a
generalisation of one of the theorems that I mentioned in my question in
the context of an ongoing development of HOL-Algebra (unfortunately, I was
not aware of this development before asking the question). Regardless, if
possible, I would appreciate if you could reconfirm that potentially you
could accept pull requests from external contributors. Nevertheless, I have
to admit, that it is unlikely that I will produce any further proofs of
results that are related to number theory in the near future.

With regard to non-technical part of your answer, previously, I used a
pseudonym xanonec on this mailing list. I also use it on Stack Overflow.
However, it seems that mailing-list-anonymous is slightly more
'professional' in some sense. Also, I am only trying to hide my real
contact details/identity from third parties (especially spam lists/online
scam/etc). There is a good reason why there is a variety of privacy
settings available on the websites like LinkedIn and Facebook and it is
possible to control who can see your posts/profile/personal information.
However, unfortunately, mailing lists do not provide such options and,
furthermore, all posts can be found via Google. In general, I prefer the
website Stack Overflow to mailing lists. However, it seems that Isabelle
community is not very active on Stack Overflow, because some of the
questions that I tried to ask there were left without a reply/comments for
days. Nevertheless, I was able to obtain a reply to the same questions
using this mailing list within hours.

Thank you

Send Cl-isabelle-users mailing list submissions to
To subscribe or unsubscribe via the World Wide Web, visit
https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users
or, via email, send a message with subject or body 'help' to
You can reach the person managing the list at
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Cl-isabelle-users digest..."
1. Re: A question about contributing to HOL
(José Manuel Rodriguez Caballero)
2. Re: A question about contributing to HOL
(Paulo Emílio de Vilhena)
3. New AFP entry: Formalization of the Embedding Path Order for
Lambda-Free Higher-Order Terms (Tobias Nipkow)
4. Re: A question about contributing to HOL (Tobias Nipkow)
----------------------------------------------------------------------
Message: 1
Date: Sun, 21 Oct 2018 13:24:18 +0200
Subject: Re: [isabelle] A question about contributing to HOL
<CAA8xVUjGOEY-CoDcuNYnMkPPLrHHg=
Content-Type: text/plain; charset="UTF-8"

Post by mailing-list anonymous
I would like to understand if it would be feasible for me to propose my

own

Post by mailing-list anonymous
contributions to HOL.

If some of your results are related to number theory, you could include
your contributions in my project of a library "number theory miscellany".
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory
But, you should include in the file either your name or a pseudonym, in
order to distinguish your contributions from my contributions. Maybe you
prefer your own miscellany, e.g., "general miscellany", "topology
miscellany", etc. In my case, my main motivation to contribute, beside the
pleasure of proving some truth, is to increase my CV, because some
reviewers of important journals, e.g., American Mathematical Monthly, said
to me that my proofs are too long to be checked and that they are annoying
for the readers (someone is confusing mathematics with comic strips). I am
successfully proving the theorems from my Master Memoir in Isabelle one by
one (work-in-progress). My first version is rather non-algorithmic, but I
have the project to include an algorithmic version in order to do explicit
computations.

Post by mailing-list anonymous
My primary concern is that I am not affiliated with an academic group or

a

Post by mailing-list anonymous
company that works with Isabelle/HOL on a regular basis. I have an
impression that all of the existing contributions to HOL were made by
people who are, somehow, officially affiliated with the Isabelle

community.
Me neither, nevertheless, the Isabelle community, at least in my case, was
the most open research community that I have ever met. Other research
communities, like the communities of pure mathematics, are rather closed
and mathematicians in general do not read the works of outsiders (they have
not time for that), e.g., the old Gauss did not read the work of the young
Abel, because he assumed that it was wrong, the old Cauchy did not read the
work of the young Galois, etc. Proof assistants are the key for an outsider
to become an insider, because the computer guarantee that the result is
fine, even if the proof is very complex. Nevertheless, I advice you to
become part of something and to change when you will be ready: the academic
growth is step by step.
Kind Regards,
José M.
------------------------------
Message: 2
Date: Sun, 21 Oct 2018 14:02:24 +0200
Subject: Re: [isabelle] A question about contributing to HOL
<
Content-Type: text/plain; charset="UTF-8"
Hello,
I’m not answering your question, but since you are working on HOL-Algebra I
would like to point out a github repository where we propose not only to
extend this library with new theories but also to revise old ones. For
instance, we already have one of the mentioned theorems you were looking
for: it is the lemma mod_ring from the theory Int_Ring (note the underline)
stated as
assumes "a ∈ carrier R - { 𝟬 }"
shows "carrier (R Quot (PIdl a)) = (λi. PIdl a +> ⟦ i ⟧) ` {0..< ¦
int_repr a ¦}"
It’s overly complicated for now, because it’s stated for all rings
isomorphic to the ring of integers, but you can easily instantiate it for
Z. We also have a theory called Multiplicative_Group_Revised where I
started an analogous development of Multiplicative_Group but more concise
since it reuses previous developments from cycles and permutations.
Other than that, there are theories on algebraic numbers, field extensions
and division of polynomials. Our most impressive result is the existence of
the algebraic closure of a field. Here is the link for the repository in
https://github.com/DeVilhena-Paulo/GaloisCVC4
Thanks,
Paulo.
Message: 4
Date: Sun, 21 Oct 2018 16:28:42 +0200
Subject: Re: [isabelle] A question about contributing to HOL
Content-Type: text/plain; charset="utf-8"
You do not have to be affiliated with anybody to contribute to
Isabelle/HOL
theories but there is no well-established process for contributing. For
small
amendments you can either send them to this mailing list or contact
individuals,
like the web page says that you found.
Larger contributions require more interaction with people who feel
responsible
for some area. In the case of Algebra, Paulo has already indicated that
there
are parellel developments that you may be able to liaise with.
Tobias

Post by mailing-list anonymous
Dear All,
I would like to understand if it would be feasible for me to propose my

own

Post by mailing-list anonymous
contributions to HOL. I have read the section "Publish contributions as

an

Post by mailing-list anonymous
external" on the Isabelle community wiki (

https://isabelle.in.tum.de/community/Publish_contributions_as_an_external
).
this

Post by mailing-list anonymous
is a general question about the possibility of a contribution being
considered, given certain specific circumstances. Thus, I believe that it
may be more useful to this mailing list, rather than
Otherwise, of course, please suggest to forward it to
.
My primary concern is that I am not affiliated with an academic group or

a

Post by mailing-list anonymous
company that works with Isabelle/HOL on a regular basis. I have an
impression that all of the existing contributions to HOL were made by
people who are, somehow, officially affiliated with the Isabelle

community.

Post by mailing-list anonymous
Thus, I would like to assess whether or not my contributions would be
considered on this basis. Of course, I am also aware of the existence of
the AFP. However, I believe, some of the theorems that I would like to
propose naturally extend some of the theories that are already available

in

Post by mailing-list anonymous
HOL and, most likely, are not suitable to be published as an independent
AFP library.
To be more specific, I would like to provide several examples of the
contributions that I would like to propose. At the moment, HOL-Algebra
"carrier (ZFact 0) = (⋃a. {{a}})"" and "ZFact_one: "carrier (ZFact 1) =
{UNIV}"". However, it does not seem to contain a lemma that could

describe

Post by mailing-list anonymous
the carrier of a more general quotient ring "ZFact (m::int)" (e.g. "0 < m
⟹ carrier (ZFact m) = {X. ∃n ∈ {0..<m}. X = {x. m dvd (x - n)}}"). Also,

I

Post by mailing-list anonymous
was not able to find a relatively standard textbook theorem that
characterises a cyclic group in terms of the quotient group "add_monoid
(ZFact m)" (e.g. "finite (carrier G) ⟹ order G = m ⟹ ∃a ∈ carrier G.
carrier G = {a[^]i | i::int. i ∈ UNIV} ⟹ add_monoid (ZFact m) ≅ G"). Some
of the potential contributions are not independent theorems, but minor
extensions of the existing lemmas in "HOL", e.g. lemma "ord_dvd_pow_eq_1"
in "Algebra-Multiplicative_Group" shows that "finite (carrier G)", "a ∈
carrier G" and "a [^] k = 𝟭" together imply "ord a dvd k", where "k" is

of

Post by mailing-list anonymous
the type "nat". However, this lemma holds even if "k" is any number of

the

Post by mailing-list anonymous
type "int" (the existing proof would need to be amended to take into
account the negative values of k).
Thank you
(I would prefer not to disclose my contact details publicly for the

reasons

Post by mailing-list anonymous
of privacy and as a measure against spam)

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/attachments/20181021/c0c48cf4/attachment.p7s
End of Cl-isabelle-users Digest, Vol 160, Issue 13
**************************************************

[Makarius]

Post by mailing-list anonymous
I am glad that it is potentially possible for me
to make contributions to HOL. However, of course, given that potentially
anyone can make a contribution, it would be nice if there was a
well-established process for making contributions.

See README_REPOSITORY. In particular:

"""
Content discipline
------------------

The following principles should be kept in mind when producing
changesets that are meant to be published at some point.

* The author of changes needs to be properly identified, using
[ui]username configuration as described above.

While Mercurial also provides means for signed changesets, we want
to keep things simple and trust that users specify their identity
correctly (and uniquely).
"""


It means you need to disclose your real name when submitting changesets.
(This is not Wikipedia where anonymous entities are allowed to do
strange things in the dark.)

Moreover it should be clear that any contribution is subject to the
existing BSD-style license scheme of the Isabelle sources: without
amendments nor exceptions.


Makarius

[José Manuel Rodriguez Caballero]

Post by mailing-list anonymous
Regardless, if
possible, I would appreciate if you could reconfirm that potentially you
could accept pull requests from external contributors.

Sure, everybody is welcome to contribute to the miscellany in number theory
(I am myself external). Also, if another person want to create another
project about miscellany, e.g., miscellany in topology, I will be glad to
contribute. I think that the best way to contribute is to make some link in
github. I have not experience about using github (maybe you have more
experience than myself in this topic). My official formation was in pure
mathematics, the computer sciences that I am doing is self-taught.

Post by mailing-list anonymous
It is good to know about the existence of this repository because it seems
that there is no mention of it in the AFP at the moment (although I cannot
be entirely certain)

I have the project to submit my results to AFP in the future, after proving
ALL the theorems from my Master Memoir. These theorems were new in the
literature, here is the video-abstract of my last publication (my goal is
to formalize everything until this level):

I have not problem to include other peoples as coauthors, because this is
the spirit of miscellany. I do not say that my theory is miscellany, what I
say is that my theory is so powerful that it can be used in order to prove
miscellany results in number theory, e.g., unexpected connections between
the semi-perimeter of a Pythagorean triangle and 2-densely divisible
numbers.

Post by mailing-list anonymous
With regard to non-technical part of your answer, previously, I used a
pseudonym xanonec on this mailing list.

Ok, you could write in your Isabelle file "xanonec" or just your name if
you want to be recognized. If your write "mailing-list anonymous" in your
Isabelle file, people evidently will think that there was a mistake of
copy-paste. Also, the problem of calling yourself "anonymous" is that
another person can call himself/herself "anonymous" too: it is like the guy
called "Anonymous" to whom many quotations are attributed. The name is just
a mask, so being anonymous is to put your mask out.

Kind Regards,
José M.

[Paulo Emílio de Vilhena]

Hi,


1.

You are right about this. While my goal was the development of Galois
Theory, the project was actually born as an attempt from me and Martin
Baillon to reduce the amount of changes to HOL-Algebra we were both making
independently.
2.

The idea is to integrate the material which could be considerate as
fundamental to any development in algebra and publish in the context of the
AFP more specific material. We already have a big part of our material in
the library and recent releases of Isabelle will come with some of my
revised theories and sophisticated tricks such as Weak_Morphisms.thy.
3.

The project was the subject of an internship in the ALEXANDRIA team,
supervised by Larry Paulson. The internship is already over and it is not
being trivial to find time to work on the project, but I do intend to
continue. The Galois correspondence theorem is certainly a milestone, but
there is a lot of work to be done on the library itself. I think it’s
preferable to progress horizontally in a proper way than to quickly prove
profound statements in a formalism that nobody will be able to use.
4.

Contributions are welcome :) I’m quite jealous with my theories and
proofs, I must say, but if you have well-founded contributions to make, I
will probably accept. By well-founded I mean that it should have at least a
minimal explanation on why such a modification would make sense. For the
moment, there are two theories in need of revision/development that may
interest you: Int_Ring.thy and Multiplicative_Group_Revised.thy. Int_Ring,
because I think that talking about rings isomorphic to Z only complicate
things and I did that to overcome a problem which does not exist anymore,
so merging Int_Ring and IntRing is something desirable.
Multiplicative_Group_Revised should just be continued.


Lastly, I would like to thank you for your interest on the project, I hope
you will be able to find and use what you need in GaloisCVC4. If you have
any suggestions or if you find that something in our formalism was not well
thought, I’m always keen to discuss.

Paulo.

Message: 2
Date: Mon, 22 Oct 2018 02:23:31 +0300
Subject: Re: [isabelle] A question about contributing to HOL
<CALaF1U+o8_1EDOy5OHEC3Rc4YcdWXjr-6Zq=
Content-Type: text/plain; charset="UTF-8"
Dear All,
In what follows, I address everyone who replied to my email (not in any
particular order).
To Tobias Nipkow,
Thank you for your reply. I am glad that it is potentially possible for me
to make contributions to HOL. However, of course, given that potentially
anyone can make a contribution, it would be nice if there was a
well-established process for making contributions.
To Paulo Emílio de Vilhena,
Thank you for your response and for providing the link to the repository
1. I would like to confirm that, while the main purpose of the project
GaloisCVC4 is the development of Galois Theory in the context of
HOL-Algebra, you are also making changes to HOL-Algebra that are not
directly related to the main line of the development of the project
GaloisCVC4, i.e. you may consider adding to the repository any established
results from algebra or making minor amendments/extensions of the existing
theorems that do not contribute to the main line of the development.
2. Furthermore, I would like to understand if your intention is to
integrate GaloisCVC4 with HOL-Algebra or publish it in the context of the
AFP.
3. Also, I would like to understand if you intend to discontinue the work
on the project after a certain deadline or after you achieve certain
milestones.
4. If my understanding of the dual purpose (see clause 1) of the project
GaloisCVC4 is correct, would you, potentially, accept pull requests from
external contributors?
Also, thank you for pointing out the existence of the (Isabelle)
generalisation of the proof of the characterisation of the carrier of Z/mZ.
I only wish I knew about the existence of GaloisCVC4 earlier.

[mailing-list anonymous]

Dear All,

I would like to thank everyone who replied to my original query. I believe
that my question was answered in full and I would like to propose (without
being insistent) to close this topic. I would also like to make several
concluding remarks in response to the replies in Digest Vol 160, Issue 15.
However, please note that I may leave further comments on this topic
without a reply.


To Makarius,

Thank you for your comment. Of course, it was not my intention to ask
whether or not I am allowed to change or ignore any of the documented
practices for making a contribution to Isabelle/HOL. My primary concern was
whether or not my contributions would be considered if I was to propose
them while not working under the supervision of one of the existing regular
co-developers of Isabelle/HOL and while not being affiliated to a
research group that regularly works with Isabelle/HOL (at the moment,
Isabelle/HOL is merely one of my past-time hobbies). I believe that this
issue has not been documented anywhere. However, as I mentioned in my
original query, I formed an impression that all of the contributions to HOL
were made by established academics in the areas of logic/formal
verification/mathematics or students working under their supervision. Thus,
I wanted to ensure that if I was going to make a proposal, it would not be
ignored/rejected because of the aforementioned circumstances.

As a side note, based on the replies given by Paulo Emílio de Vilhena (see
below), if I decide to submit my contributions to the community, it is
likely that I will try to do so indirectly through the repository
GaloisCVC4 (also, see the next section in my reply).


To Makarius and José Manuel Rodriguez Caballero,

I have no intention to hide my identity from the regular users of this
mailing list. However, I would prefer to remain anonymous to the general
public. Of course, anyone who needs to know my name/contact details for any
good reason can inquire about them in a personal email (with the
understanding that they are not to be shared without my consent). Also, of
course, it is in my interest to associate my name with my contributions if
they are to be accepted (whether they are contributions to Isabelle/HOL or
a private repository of an academic).


To Paulo Emílio de Vilhena,

Thank you for the detailed reply.

I would like to make several comments with regard to clause 4 in your reply:
1. Firstly, given that you have already introduced (or seem to be working
on) a significant number of the contributions that I was going to propose,
it seems now that it is slightly less likely that I will make any attempts
to make contributions in the very near future.
2. I have a certain amount of experience in computer programming and I am
familiar with the feeling that one can get when an external entity with
less experience is trying to 'sabotage' your code base or your intended
direction for the development. Luckily, at least, it is nearly impossible
to introduce errors/bugs in Isabelle theorems. If I will ever make an
attempt to make a contribution, then I will also make every attempt to
ensure that it is either peripheral to the main line of the development or,
at least, it is very unlikely to have any negative impact on the main line
of the development. Of course, I would submit a pull request on GitHub and
you are welcome to reject it if you decide that it is not suitable
(obviously, if you do decide to reject it, I will appreciate any
constructive feedback).
If there was an active issue tracker for the project, I would also be glad
to look into the problems that you would like to be solved, but you believe
that they have a low priority (i.e. the problems that you would not want to
spend your time on). However, most certainly, I cannot guarantee my
commitment (as I mentioned somewhere in this reply, at the moment,
Isabelle/HOL is merely one of my past-time hobbies). Thus, please do not
start an issue tracker on my behalf :).
3. "I think that talking about rings isomorphic to Z only complicate
things...". I cannot imagine that anyone who is able to understand the
content of HOL-Algebra will not be able to specialise theorems in Int_Ring
to their needs. However, most certainly, it would be useful not to expect
the users to specialise the results to Z in almost every individual library
that uses Int_Ring (in all probability, Z would be a very common
application of theorems in Int_Ring).


To José Manuel Rodriguez Caballero,

Thank you for providing further information and for the confirmation that
you may be able to accept pull requests. Based on the latest reply by Paulo
Emílio de Vilhena, it seems that it is much more likely that I will be
(potentially) submitting my contributions to GaloisCVC4, because, I
believe, my (potential) contributions are more suitable for a library that
is closely associated with HOL-Algebra than a library in the area of number
theory. However, if any of my contributions will be rejected (for any
reason other than the quality of my proofs or originality) or if I will
ever formalise anything that may be more suitable for your repository, I
will let you know.


Thank you

Send Cl-isabelle-users mailing list submissions to
To subscribe or unsubscribe via the World Wide Web, visit
https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users
or, via email, send a message with subject or body 'help' to
You can reach the person managing the list at
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Cl-isabelle-users digest..."
1. Re: Potential problems with socket I/O after Ubuntu update
(Makarius)
2. Re: A question about contributing to HOL (Makarius)
3. Re: A question about contributing to HOL
(José Manuel Rodriguez Caballero)
4. Re: A question about contributing to HOL
(Paulo Emílio de Vilhena)
5. Fwd: NFM 2019 Second Call For Papers- 11th Annual NASA
Formal Methods Symposium (Rohit Dureja)
----------------------------------------------------------------------
Message: 1
Date: Mon, 22 Oct 2018 12:54:19 +0200
Subject: Re: [isabelle] Potential problems with socket I/O after
Ubuntu update
Content-Type: text/plain; charset=utf-8

Until the situation becomes worse, e.g. Ubuntu 18.10 other Linux
distributions with non-working kernel, I will not venture on
producing
another Isabelle release just to workaround problems on Ubuntu
18.04.1.

I'm using the LTS versions of Ubuntu ... this thread on the mailing
list has prevented me from upgradig so far, in order to avoid getting
an unusable Isabelle.
So what to do after upgrading, if I need a usable Isabelle2018?

On 05/10/2018 01:50, Makarius wrote:>

The critical package is: linux-image-4.15.0-36-generic
The previous version still works: linux-image-4.15.0-34-generic
Is there anybody who can confirm the problem with Ubuntu Linux Kernel
4.15.0-36? And that it works again after downgrading the package?

"""
Warning: potential problem with Ubuntu Linux 18.04
The kernel update linux-image-4.15.0-36-generic (Oct-2018) introduces a
timing problem with socket communication in the Isabelle Prover IDE,
notably Isabelle/jEdit. Thus loading big sessions becomes very slow
(e.g. theory HOL-Library.Library or HOL-Analysis.Analysis). This can be
avoided by downgrading to linux-image-4.15.0-34-generic or by using the
following temporary workaround for Isabelle2018.
https://isabelle.in.tum.de/Isabelle_05-Oct-2018/Isabelle_05-Oct-2018_app.tar.gz
"""
Makarius
------------------------------
Message: 2
Date: Mon, 22 Oct 2018 13:06:41 +0200
Subject: Re: [isabelle] A question about contributing to HOL
Content-Type: text/plain; charset=utf-8

I am glad that it is potentially possible for me
to make contributions to HOL. However, of course, given that potentially
anyone can make a contribution, it would be nice if there was a
well-established process for making contributions.

"""
Content discipline
------------------
The following principles should be kept in mind when producing
changesets that are meant to be published at some point.
* The author of changes needs to be properly identified, using
[ui]username configuration as described above.
While Mercurial also provides means for signed changesets, we want
to keep things simple and trust that users specify their identity
correctly (and uniquely).
"""
It means you need to disclose your real name when submitting changesets.
(This is not Wikipedia where anonymous entities are allowed to do
strange things in the dark.)
Moreover it should be clear that any contribution is subject to the
existing BSD-style license scheme of the Isabelle sources: without
amendments nor exceptions.
Makarius
------------------------------
Message: 3
Date: Mon, 22 Oct 2018 07:54:57 -0400
Subject: Re: [isabelle] A question about contributing to HOL
<
Content-Type: text/plain; charset="UTF-8"

Regardless, if
possible, I would appreciate if you could reconfirm that potentially you
could accept pull requests from external contributors.

Sure, everybody is welcome to contribute to the miscellany in number theory
(I am myself external). Also, if another person want to create another
project about miscellany, e.g., miscellany in topology, I will be glad to
contribute. I think that the best way to contribute is to make some link in
github. I have not experience about using github (maybe you have more
experience than myself in this topic). My official formation was in pure
mathematics, the computer sciences that I am doing is self-taught.

It is good to know about the existence of this repository because it

seems

that there is no mention of it in the AFP at the moment (although I

cannot

be entirely certain)

I have the project to submit my results to AFP in the future, after proving
ALL the theorems from my Master Memoir. These theorems were new in the
literature, here is the video-abstract of my last publication (my goal is
http://youtu.be/Ms9lrm4wLDQ
I have not problem to include other peoples as coauthors, because this is
the spirit of miscellany. I do not say that my theory is miscellany, what I
say is that my theory is so powerful that it can be used in order to prove
miscellany results in number theory, e.g., unexpected connections between
the semi-perimeter of a Pythagorean triangle and 2-densely divisible
numbers.

With regard to non-technical part of your answer, previously, I used a
pseudonym xanonec on this mailing list.

Ok, you could write in your Isabelle file "xanonec" or just your name if
you want to be recognized. If your write "mailing-list anonymous" in your
Isabelle file, people evidently will think that there was a mistake of
copy-paste. Also, the problem of calling yourself "anonymous" is that
another person can call himself/herself "anonymous" too: it is like the guy
called "Anonymous" to whom many quotations are attributed. The name is just
a mask, so being anonymous is to put your mask out.
Kind Regards,
José M.
------------------------------
Message: 4
Date: Mon, 22 Oct 2018 14:37:03 +0200
Subject: Re: [isabelle] A question about contributing to HOL
<
Content-Type: text/plain; charset="UTF-8"
Hi,
1.
You are right about this. While my goal was the development of Galois
Theory, the project was actually born as an attempt from me and Martin
Baillon to reduce the amount of changes to HOL-Algebra we were both
making
independently.
2.
The idea is to integrate the material which could be considerate as
fundamental to any development in algebra and publish in the context of
the
AFP more specific material. We already have a big part of our material
in
the library and recent releases of Isabelle will come with some of my
revised theories and sophisticated tricks such as Weak_Morphisms.thy.
3.
The project was the subject of an internship in the ALEXANDRIA team,
supervised by Larry Paulson. The internship is already over and it is
not
being trivial to find time to work on the project, but I do intend to
continue. The Galois correspondence theorem is certainly a milestone,
but
there is a lot of work to be done on the library itself. I think it’s
preferable to progress horizontally in a proper way than to quickly
prove
profound statements in a formalism that nobody will be able to use.
4.
Contributions are welcome :) I’m quite jealous with my theories and
proofs, I must say, but if you have well-founded contributions to make,
I
will probably accept. By well-founded I mean that it should have at
least a
minimal explanation on why such a modification would make sense. For the
moment, there are two theories in need of revision/development that may
interest you: Int_Ring.thy and Multiplicative_Group_Revised.thy.
Int_Ring,
because I think that talking about rings isomorphic to Z only complicate
things and I did that to overcome a problem which does not exist
anymore,
so merging Int_Ring and IntRing is something desirable.
Multiplicative_Group_Revised should just be continued.
Lastly, I would like to thank you for your interest on the project, I hope
you will be able to find and use what you need in GaloisCVC4. If you have
any suggestions or if you find that something in our formalism was not well
thought, I’m always keen to discuss.
Paulo.

Message: 2
Date: Mon, 22 Oct 2018 02:23:31 +0300
Subject: Re: [isabelle] A question about contributing to HOL
<CALaF1U+o8_1EDOy5OHEC3Rc4YcdWXjr-6Zq=
Content-Type: text/plain; charset="UTF-8"
Dear All,
In what follows, I address everyone who replied to my email (not in any
particular order).
To Tobias Nipkow,
Thank you for your reply. I am glad that it is potentially possible for

me

to make contributions to HOL. However, of course, given that potentially
anyone can make a contribution, it would be nice if there was a
well-established process for making contributions.
To Paulo Emílio de Vilhena,
Thank you for your response and for providing the link to the repository
1. I would like to confirm that, while the main purpose of the project
GaloisCVC4 is the development of Galois Theory in the context of
HOL-Algebra, you are also making changes to HOL-Algebra that are not
directly related to the main line of the development of the project
GaloisCVC4, i.e. you may consider adding to the repository any

established

results from algebra or making minor amendments/extensions of the

existing

theorems that do not contribute to the main line of the development.
2. Furthermore, I would like to understand if your intention is to
integrate GaloisCVC4 with HOL-Algebra or publish it in the context of the
AFP.
3. Also, I would like to understand if you intend to discontinue the work
on the project after a certain deadline or after you achieve certain
milestones.
4. If my understanding of the dual purpose (see clause 1) of the project
GaloisCVC4 is correct, would you, potentially, accept pull requests from
external contributors?
Also, thank you for pointing out the existence of the (Isabelle)
generalisation of the proof of the characterisation of the carrier of

Z/mZ.

I only wish I knew about the existence of GaloisCVC4 earlier.

------------------------------
Message: 5
Date: Mon, 22 Oct 2018 23:05:20 -0500
Subject: [isabelle] Fwd: NFM 2019 Second Call For Papers- 11th Annual
NASA Formal Methods Symposium
<CADByozH7joejq_Swys1dbEq83+VtHx8oRrHg36ieehek=
Content-Type: text/plain; charset="UTF-8"
****************************************************
The Eleventh NASA Formal Methods Symposium
https://robonaut.jsc.nasa.gov/R2/pages/nfm2019.html
7 - 9 May 2019
Rice University, Houston, Texas, USA
****************************************************
-----------------------
The widespread use and increasing complexity of mission-critical and
safety-critical systems at NASA and in the aerospace industry require
advanced techniques that address these systems' specification, design,
verification, validation, and certification requirements. The NASA
Formal Methods Symposium (NFM) is a forum to foster collaboration
between theoreticians and practitioners from NASA, academia, and
industry. NFM's goals are to identify challenges and to provide
solutions for achieving assurance for such critical systems.
New developments and emerging applications like autonomous software for
uncrewed deep space human habitats, caretaker robotics, Unmanned Aerial
Systems (UAS), UAS Traffic Management (UTM), and the need for
system-wide fault detection, diagnosis, and prognostics provide new
challenges for system specification, development, and verification
approaches. The focus of these symposiums are on formal techniques and
other approaches for software assurance, including their theory, current
capabilities and limitations, as well as their potential application to
aerospace, robotics, and other NASA-relevant safety-critical systems
during all stages of the software life-cycle.
The NASA Formal Methods Symposium is an annual event organized by the
NASA Formal Methods (NFM) Steering Committee, comprised of researchers
spanning several NASA centers. NFM 2019
(https://robonaut.jsc.nasa.gov/R2/pages/nfm2019.html) is being
co-organized by Rice University and NASA- Johnson Space Center in
Houston, TX.
-------------------
We encourage submissions on cross-cutting approaches that bring together
formal methods and techniques from other domains such as probabilistic
reasoning, machine learning, control theory, robotics, and quantum
computing among others.
* Formal verification, including theorem proving, model checking,
and static analysis
* Advances in automated theorem proving including SAT and SMT solving
* Use of formal methods in software and system testing
* Run-time verification
* Techniques and algorithms for scaling formal methods, such as
abstraction and symbolic methods, compositional techniques, as well as
parallel and/or distributed techniques
* Code generation from formally verified models
* Safety cases and system safety
* Formal approaches to fault tolerance
* Theoretical advances and empirical evaluations of formal methods
techniques for safety-critical systems, including hybrid and embedded
systems
* Formal methods in systems engineering and model-based development
* Correct-by-design controller synthesis
* Formal assurance methods to handle adaptive systems
----------------
Abstract Submission: 7 Dec 2018
Paper Submission: 14 Dec 2018
Paper Notifications: 22 Feb 2019
Camera-ready Papers: 22 Mar 2019
Symposium: 7-9 May 2019
----------------
The symposium will take place in the McMurtry Auditorium, Rice
University, Houston, Texas, USA, May 7--9, 2019.
There will be no registration fee for participants. All interested
individuals, including non-US citizens, are welcome to attend, to listen
to the talks, and to participate in discussions; however, all attendees
must register.
-------------------
1. Regular papers describing fully developed work and complete
results (15 pages + references)
2. Two categories of short papers: (6 pages + references)
(a) Tool Papers describing novel, publicly-available tools
(b) Case Studies detailing complete applications of formal methods
to real systems with publicly-available artifacts
All papers should be in English and describe original work that has not
been published or submitted elsewhere. All submissions will be fully
reviewed by members of the Programme Committee. Papers will appear in a
volume of Springer's Lecture Notes on Computer Science (LNCS), and must
use LNCS style formatting. Papers should be submitted in PDF format
here: https://easychair.org/conferences/?conf=nfm2019.
-----------------
* Virginie Wiels, ONERA, France
* Richard Murray, CalTech, USA
* NASA Panel: Challenges for Future Exploration
-----------
Moshe Y. Vardi (General Chair)
Julia Badger (PC Chair)
Kristin Yvonne Rozier (PC Chair)
--------------------
Erika Ábrahám, RWTH Aachen University, Germany
Dirk Beyer, LMU Munich, Germany
Armin Biere, Johannes Kepler University Linz, Austria
Nikolaj Bjorner, Microsoft, USA
Sylvie Boldo, INRIA, France
Jonathan Bowen, London South Bank University, UK
Gianfranco Ciardo, Iowa State University, US
Darren Cofer, Rockwell Collins, USA
Frederic Dadeau, FEMTO-ST, France
Ewen Denney, NASA, US
Gilles Dowek, INRIA and ENS Paris-Saclay, France
Steven Drager, AFRL, US
Catherine Dubois, ENSIIE-Samovar, France
Alexandre Duret-Lutz, LRDE/EPITA, France
Aaron Dutle, NASA, US
Marco Gario, Siemens Corporate Technology, USA
Alwyn Goodloe, NASA, US
Arie Gurfinkel, University of Waterloo, Canada
John Harrison, Amazon Web Services, USA
Klaus Havelund, JPL/NASA, USA
Constance Heitmeyer, Naval Research Laboratory, USA
Marieke Huisman, University of Twente, The Netherlands
Shafagh Jafer, Embry-Riddle University, USA
Xiaoqing Jin, Toyota Technical Center, USA
Rajeev Joshi, JPL/NASA, USA
Laura Kovacs, Vienna University of Technology, Austria
Joe Leslie-Hurd, Intel, US
Panagiotis Manolios, Northeastern University, USA
Cristian Mattarei, Stanford University, US
Stefan Mitsch, Carnegie Mellon University, US
Cesar Munoz, NASA, US
Anthony Narkawicz, NASA, US
Necmiye Ozay, University of Michigan, USA
Corina Pasareanu, CMU/NASA, USA
Lee Pike, USA
Johann Schumann, SGT, USA
Cristina Seceleanu, Malardalen University, Sweden
Bernhard Steffen, University of Dortmund, Germany
Stefano Tonetta, FBK-IRST, Italy
Ufuk Topcu, University of Texas at Austin, USA
Christoph Torens, German Aerospace Center, Germany
Michael Watson, NASA, USA
Huan Xu, University of Maryland, US
End of Cl-isabelle-users Digest, Vol 160, Issue 15
**************************************************