[isabelle-dev] Proper sign of gcd / lcm on type int
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") * PolyML.IntInf.gcd: always >= 0 PolyML.IntInf.lcm: mixed signs, according to product of arguments * Integer.gcd / lcm: mixed signs -- IIRC the implementation was only meant to operate on "nat", which happens to be spelled "int" in ML. My impression is that the HOL definitions are canonical: several number theory experts have gone over it over the years. Is this correct? An investigation of the (very few) uses of the above Poly/ML and Isabelle/ML operations in Isabelle + AFP supports the following working hypothesis: Integer.gcd / lcm should follow the HOL versions, in "normalizing" the sign, i.e. removing it. (The updated implementation will use PolyML.IntInf gcd for improved performance.) Does this sound like a good idea? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] problem with Nominal in the AFP
> 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. In the absence of a more formalized connection between Isabelle and AFP changesets, guesswork is all we can do, and it will always fail in some situations. (For now I'm not suggesting we should add a more formalized connection.) Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] problem with Nominal in the AFP
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 repositories. 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. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] problem with Nominal in the AFP
> 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] problem with Nominal in the AFP
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 * thm)) * local_theory
***Argument: lthy : local_theory
***Reason:
*** Can't unify local_theory to Attrib.binding * term (Incompatible types)
*** ML error (line 60 of "~~/afp/thys/Nominal2/nominal_atoms.ML"):
*** Pattern and expression have incompatible types.
***Pattern: ((_, (_, permute_ldef)), lthy) : ('a * ('b * 'c)) * 'd
***Expression:
*** Specification.definition NONE []
*** ((permute_def_name, [...]), permute_eqn)
*** lthy
*** : local_theory -> (term * (string * thm)) * local_theory
***Reason:
*** Can't unify ('a * ('b * 'c)) * 'd to
*** local_theory -> (term * (string * thm)) * local_theory
*** (Incompatible types)
*** ML error (line 63 of "~~/afp/thys/Nominal2/nominal_atoms.ML"):
*** Type error in function application.
***Function: Specification.definition NONE [] :
*** term list ->
*** Attrib.binding * term ->
*** local_theory -> (term * (string * thm)) * local_theory
***Argument: ((atom_def_name, []), atom_eqn) : (binding * 'a list) * term
***Reason:
*** Can't unify term list to (binding * 'a list) * term
*** (Incompatible types)
*** ML error (line 62 of "~~/afp/thys/Nominal2/nominal_atoms.ML"):
*** Pattern and expression have incompatible types.
***Pattern: ((_, (_, atom_ldef)), lthy) : ('a * ('b * 'c)) * 'd
***Expression:
*** Specification.definition NONE [] ((atom_def_name, [...]), atom_eqn)
*** lthy
*** : local_theory -> (term * (string * thm)) * local_theory
***Reason:
*** Can't unify ('a * ('b * 'c)) * 'd to
*** local_theory -> (term * (string * thm)) * local_theory
*** (Incompatible types)
*** At command "ML_file" (line 3433 of "~~/afp/thys/Nominal2/Nominal2_Base.thy")
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP/MFMC_Countable still failing
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 +0200, Makarius wrote: > As of Isabelle/dd6cd88cebd9 + AFP/8186added238, MFMC_Countable is > still > failing. > > As a new entry it might be actually easy to upgrade. > > Afterwards we might be back to the rare situation where Isabelle + > AFP > fully work. > > > Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
