Re: [isabelle-dev] problem with Nominal in the AFP

[Lars Hupel]

> 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

[Makarius]

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

[Lars Hupel]

> 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

[Lawrence Paulson]

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