[isabelle-dev] Global constant names in inductive

2017-04-06 Thread Lars Hupel
Dear list, while poking around in the function package (to store more information in "info"), I also realized that I need a little bit more information from the inductive package. Reading its sources, I stumbled upon 10-year-old comments by Makarius that remind the reader of (what I assume is) no

Re: [isabelle-dev] Global constant names in inductive

2017-04-06 Thread Lars Hupel
> I'm at a loss for an explanation. Does anybody have any idea what is > going on there? I now have an updated patch that instead of changing "add_inductive_global" to use "open_target"/"close_target" leaves it unchanged. With this, HOL-Proofs-Lambda and everything else goes through.

Re: [isabelle-dev] Global constant names in inductive

2017-04-06 Thread Makarius
On 06/04/17 09:29, Lars Hupel wrote: > while poking around in the function package (to store more information > in "info"), I also realized that I need a little bit more information > from the inductive package. > > Reading its sources, I stumbled upon 10-year-old comments by Makarius > that remin

Re: [isabelle-dev] Global constant names in inductive

2017-04-06 Thread Lars Hupel
> Did you encounter an actual problem from that situation? > > Formally, a comment is not a problem. "Fixing" such things prematurely > is likely to break it. Yes, there is an actual problem. I define a function via "Function.add_function" and inspect the resulting info. As per usual discipline t

Re: [isabelle-dev] Global constant names in inductive

2017-04-06 Thread Makarius
On 06/04/17 13:08, Lars Hupel wrote: >> Did you encounter an actual problem from that situation? >> >> Formally, a comment is not a problem. "Fixing" such things prematurely >> is likely to break it. > > Yes, there is an actual problem. I define a function via > "Function.add_function" and inspect

Re: [isabelle-dev] Global constant names in inductive

2017-04-06 Thread Lars Hupel
> Your proposed change > https://isabelle.in.tum.de/repos/testboard/rev/20d5e446aa10 looks > formally OK. See now Isabelle/3c628937899d and AFP/a7160ffc25f1. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.

[isabelle-dev] Fwd: Build of AFP entry Incompleteness failed

2017-04-06 Thread Lawrence Paulson
A very weird error has somehow appeared Larry > Begin forwarded message: > > From: Isabelle/Jenkins > Subject: Build of AFP entry Incompleteness failed > Date: 6 April 2017 at 18:02:58 BST > To: l...@cam.ac.uk > > *** Failed to load theory "Nominal2_Abs" (unresolved "Nominal2_Base") > *** Faile

Re: [isabelle-dev] Fwd: Build of AFP entry Incompleteness failed

2017-04-06 Thread Lars Hupel
> A very weird error has somehow appeared That was due to my change in inductive. It's all resolved now. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev