Dear integer experts,
presently on Isabelle/c3896c385c3e and AFP/d9305abd02e9, I am trying to
understand the situation of gcd / lcm for negative arguments.
We have the following slightly divergent operations:
* HOL gcd / lcm: always >= 0 (via "normalize" which is "abs")
*
> Apart from that, there is also a custom to push AFP changes a bit later
> than the ones on the Isabelle repository. Maybe Jenkins can take this
> somehow into account and not start tests on AFP immediately.
I've thought about this. The problem is that the notion of "a bit later"
is ill-defined.
On 31/05/16 11:18, Lars Hupel wrote:
>> Incompleteness FAILED
>
> This problem has already been addressed. Makarius changed some Isabelle
> signatures in Isabelle/4d04e14d7ab8, and adapted AFP in d46ea7497f.
>
> Unfortunately it's currently impossible to perform atomic changes to
> both
> Incompleteness FAILED
This problem has already been addressed. Makarius changed some Isabelle
signatures in Isabelle/4d04e14d7ab8, and adapted AFP in d46ea7497f.
Unfortunately it's currently impossible to perform atomic changes to
both repositories.
Cheers
Lars
Incompleteness FAILED
(see also
/media/data/jenkins/workspace/isabelle-repo-afp/heaps/polyml-5.6_x86_64-linux/log/Incompleteness)
*** Specification.definition NONE [] ((permute_def_name, []), permute_eqn)
*** : Attrib.binding * term ->
*** local_theory -> (term * (string *
Unfortunately it is not easily upgraded, as I did a semantic change in
HOL-Probability (i.e. ereal -> ennreal).
My local version of MFMC is currently 25% ported, and I hope to be
finished in a couple of days. (I didn't work on it over the long
weekend)
- Johannes
On Mo, 2016-05-30 at 23:28
