Re: [isabelle-dev] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken

[Dmitriy Traytel]

Hi Makarius,

> On 1 Jun 2018, at 23:32, Makarius  wrote:
> 
> On 01/06/18 10:35, Dmitriy Traytel wrote:
>> Hi all,
>> 
>> thanks for pointing this out, Lars. And thanks for looking at the sources, 
>> Jasmin.
>> 
>> The problem seems to only show up when the declaration in question is inside 
>> of a class context. Here is a reduced version that does not involve primrec 
>> at all.
>> 
>> context linorder begin
>> 
>> context fixes b :: nat begin
>> 
>> definition c where "c = b"
>> 
>> end
>> 
>> end
> 
> This is ultimately a problem of the class target in conjunction with the
> unnamed local context. See now
> 
> changeset:   68351:bcdc4c21ab1d
> tag: tip
> user:wenzelm
> date:Fri Jun 01 22:01:43 2018 +0200
> files:   src/Pure/Isar/class.ML
> description:
> varify frees, notably dangling_params (see also e0cd57aeb60c);

Happy to see that this was not a problem in our codebase.


>> @Makarius: What is the rationale behind disallowing the definition of c?
> 
> The changeset explains it as follows:
> 
> changeset:   68239:e0cd57aeb60c
> user:wenzelm
> date:Sun May 20 22:37:00 2018 +0200
> files:   src/Pure/global_theory.ML
> description:
> more checks for global facts: disallow undeclared frees (as in
> Export_Theory.export_fact);
> 
> 
> At first I did not want to expose odd mixtures of free vs. schematic
> variables to the world out there, and for global items we have a clear
> understanding that fixed vs. schematic can always be flipped via
> Logic.varify_global/unvarify_global and related operations.
> 
> Moreover, the check was meant to tighten existing tools and local theory
> targets, as we have seen here. In the process, I had to give up the full
> rigour, though: a3bd410db5b2 allows mixed variable indexes.
> 
> 
> Looking even more closely at global facts, there might be further
> problems that are still undetected. In the next round I will experiment
> with Thm.plain_prop_of to see if we can disallow hyps, shyps, tpairs.

Thanks for the explanation. The context handling in the BNF packages has quite 
improved over the years thanks to the additional checks you introduce every now 
and then. Do not hesitate to tell us should you encounter further problems.

Dmitriy



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken

[Dmitriy Traytel]

Hi all,

thanks for pointing this out, Lars. And thanks for looking at the sources, 
Jasmin.

The problem seems to only show up when the declaration in question is inside of 
a class context. Here is a reduced version that does not involve primrec at all.

context linorder begin

context fixes b :: nat begin

definition c where "c = b"

end

end

@Makarius: What is the rationale behind disallowing the definition of c? Or is 
this not an expected behavior?

Dmitriy

> On 31 May 2018, at 11:17, Blanchette, J.C.  wrote:
> 
> Hi Lars,
> 
> Thanks for the heads-up. Makarius's change e0cd57aeb60c is clearly the 
> immediate source of the problem, but the more profound cause seems to be some 
> nonstandard handling of variables. The "illegal fixed variable" in question, 
> "s1", seems to originate from line 397 in "bnf_fp_n2m.ML":
> 
>  |> Variable.add_fixes (mk_names n "s")
> 
> Dmitriy, since this is your code, could you take a look at it? The line in 
> question seems to have been added as part of an optimization you did in 2016 
> (see 8053ef5a0174).
> 
> Cheers,
> 
> Jasmin
> 
>> On 31. May 2018, at 10:28, Lars Hupel  wrote:
>> 
>> since approximately Isabelle/e0cd57aeb60c (~1 week):
>> 
>> *** Malformed global fact
>> "Misc_N2M.linorder_class.f1_t.n2m_t_ctor_fold_dict"
>> *** Illegal fixed variable: "s1"
>> *** At command "primrec" (line 164 of
>> "~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy")
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] the new "imports" semantics

[Dmitriy Traytel]

Hi Larry,

in ~~/src/HOL/ROOT, the theory Probability is declared as "global". That means 
that you must import it without any session qualification (just like Main or 
Complex_Main).

Dmitriy

> On 2 Nov 2017, at 17:47, Lawrence Paulson  wrote:
> 
> I’ve been converting some theories from the old pathname syntax to the new 
> setup. I have the line
> 
>   imports "HOL-Probability.Probability”
> 
> but it is rejected with the message
> 
>   Bad theory import "HOL-Probability.Probability"
> 
> If instead I import "HOL-Probability.Random_Permutations” or 
> "HOL-Probability.Central_Limit_Theorem” it works fine. And I have triple 
> checked that Probability is spelt correctly. Any hints?
> 
> Larry
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] map/rel/set for lift_bnf

[Dmitriy Traytel]

Hi Lars,

thanks for the reminder. Cf. c6714a9562ae and a5a24e1a6d6f.

Note that this still doesn’t provide the interface to Lifting and Transfer via 
transfer rules for the BNF constants (which is more complicated since lift_bnf 
doesn’t know about Lifting, in particular about the correspondence relations).

Dmitriy


> On 11 Jul 2017, at 16:18, Lars Hupel  wrote:
> 
> Dear BNF experts,
> 
> a while ago [0] I posted some comments on the "lift_bnf" command. I'm
> currently in the process of cleaning up the "Finite_Map" theory and
> found out that now, "lift_bnf" exports the definitional theorems for
> map/rel/set.
> 
> In this case, the theorem looks like this:
> 
> fmmap ≡ λf. Abs_fmap ∘ Finite_Map.fmap.fun.map_fun f ∘ fmlookup
> 
> But if I look at "BNF_Def.map_def_of_bnf", the theorem looks like this:
> 
> fmmap ≡ λf. Abs_fmap ∘ op ∘ (map_option f) ∘ fmlookup
> 
> I couldn't find any way to unfold "Finite_Map.fmap.fun.map_fun" (which
> is presumably some internal constant), which means I still have to use
> the workaround of manually registering the lemmas I want.
> 
> This is not urgent, but it would be cool if I could get rid of the
> workaround for Isabelle2017.
> 
> Cheers
> Lars
> 
> 
> [0]
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Uses of Jenkins at TUM

[Dmitriy Traytel]

Hi Makarius,

> On 24 Apr 2017, at 18:12, Makarius  wrote:
> 
> On 24/04/17 14:46, Makarius wrote:
>> 
>> Are there users of it outside the TUM group?

My usage is the same as in Jasmin’s and Andreas’ case.

>> 
>> What is good about it? What is bad about it?
> 
> (1) To follow the line of Mira vs. Jenkins:
> 
>  * My main use of Mira was to figure out which Isabelle version
> corresponds to which AFP version, when something was broken in AFP.
> 
>  * I did not find this information in Jenkins, when I was still
> spending more time on it last year.

It is there on the status page: 
https://ci.isabelle.systems/jenkins/job/afp-repo-afp/827/

> Revision: c05bec5d01ad6660f7825f6a8315f9aa350a7a67
> Revision: fd20a4c244d80bf87ea3f367c66c93b6164c85ce

And it was there from the beginning: 
https://ci.isabelle.systems/jenkins/job/afp-repo-afp/1/ 


It would help if we would not need to guess which id is for isabelle and which 
one is for the AFP though (although this is easy to figure out).

> 
>  * For actual quasi-interactive testing I always use "isabelle build"
> directly on a local or remote machine, with incrementally updated global
> build state (heaps and logs). Here it is important to get results within
> approx. 20-30 min -- presently we are at > 30 min.

Since I usually change things early in HOL (around BNF_Def), incremental builds 
would not save a lot. I think the time spend on non-HOL logics is not zero but 
negligible.

Dmitriy


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Discovering named_theorems

[Dmitriy Traytel]

Hi Makarius,

> On 10 May 2016, at 22:48, Makarius <makar...@sketis.net> wrote:
> 
> On 03/03/16 14:19, Dmitriy Traytel wrote:
> 
>> I wondered whether named_theorems (or more generally all dynamic facts) 
>> deserve to be more visible. In particular when I search for
>> 
>>  "(?a < ?c - ?b) = (?a + ?b < ?c)”
>> 
>> with find_theorems, I’d like to be reminded of algebra_simps (instead or 
>> rather in addition to Groups.ordered_ab_group_add_class.less_diff_eq).
>> 
>> Looking at the named_theorems that we have today (with grep), I see two 
>> kinds: those relevant for the working formalizer (algebra_simps, 
>> derivative_intros, ...), and those mostly relevant for tools (transfer_raw, 
>> …). It would be good to make the former ones easily discoverable (via 
>> find_theorems, potentially also Sledgehammer). If something is really 
>> irrelevant for the working formalizer, it(s binding) could in principle be 
>> concealed (preventing find_theorems from showing it).
> 
> See now the following change:
> 
> changeset:   63080:8326aa594273
> tag: tip
> user:wenzelm
> date:Tue May 10 22:25:06 2016 +0200
> files:   src/Pure/Isar/proof_context.ML
> src/Pure/Tools/find_theorems.ML src/Pure/facts.ML
> description:
> find dynamic facts as well, but static ones are preferred;
> tuned;
> 
> 
> It is not precisely what you have described, but it is a
> straight-forward continuation of the existing fact retrieval.
> 
> Note that the "Duplicates" option makes a difference if dynamic facts
> actually show up. The details of these policies are from a different
> continent, and not totally clear to me.
> 
>> PS: The real reason why I am interested in this is that in the forthcoming 
>> package for non-primitive corecursion (joint work with Jasmin Blanchette, 
>> Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu), we would like to 
>> generate dynamic theorems for coinduction up to congruence (because the 
>> coinduction principles gets stronger with every non-primitively corecursive 
>> function defined). But this only makes sense if users are aware of those 
>> dynamic theorems, i.e. can find them easily.
> 
> Is the above sufficient for this application?

Yes, thanks!

Ticking “Duplicates” makes the result even more as I expected. But I can 
imagine that showing no duplicates (with static theorems preferred) is a 
reasonable default.

Dmitriy


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Highlighting of entity def/ref positions

[Dmitriy Traytel]

Hi Makarius,

this is nice. At first I was a bit surprised to see the first occurrence of 
list, Nil, and Cons in blue in the following datatype definitions.

datatype 'a list = Nil | Cons 'a "'a list”

But I guess, it makes sense to indicate that this is a new thing being defined.

The question is whether the list on the right hand side of the above datatype 
should also be blue (as in fun the recursive occurrences are also blue). IIRC, 
we are doing some context tricks to make it look black (Jasmin knows better).

Dmitriy


> On 18 Apr 2016, at 16:24, Makarius  wrote:
> 
> *** Prover IDE -- Isabelle/Scala/jEdit ***
> 
> * Highlighting of entity def/ref positions wrt. cursor.
> 
> 
> This refers to Isabelle/15e6ae52e91a, where it is pushed through most 
> definitional packages already.
> 
> Name bindings need to be treated carefully with their position information, 
> but it also needs to be reset in certain situations (typically for derived 
> fact names).
> 
> 
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins updates

[Dmitriy Traytel]

Hi Lars,

thanks for your work. Unfortunately, currently pushing to testboard/isabelle 
does not seem to trigger new builds. Is this related to the job renamings? 
Another renaming issue is visible here:

https://ci.isabelle.systems/status/

The status icon still points to (the now non-existent) isabelle-repo-checkin .

Dmitriy

> On 19 Mar 2016, at 19:16, Lars Hupel  wrote:
> 
> Dear Isabelle developers,
> 
> I've made another round of changes to the Jenkins setup today.
> 
> * There is now a nightly "benchmark" job which runs everything in
> ~~/src/Benchmarks, as promised [0].
> 
> * Due to more spurious failures, I've switched over the build machines
> to use 64bit. Previous discussions on the mailing list about this were
> unclear about the resolution, so I'm opting for 64bit to give the ML
> process even more space. Until I can confirm that the builds are running
> smoothly there, the build notification mails stay disabled.
> 
> * Renamed some jobs to make more apparent what they do. The rule is: If
> a job's name is a prefix of another job's name, the first one triggers
> the second one. For example, the "afp-repo" triggers the "afp-repo-afp"
> job, and does nothing else.
> 
> * The new build script ("isabelle ci_build") has already been running
> for a while and will soon be merged into the ~~/Admin folder of the
> repository, as suggested by Makarius. This script will then also take
> care of sending afptest-style mails, but only after the builds are
> stable (see above).
> 
> Cheers
> Lars
> 
> 
> [0]
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Local_Theory.restore versus Local_Theory.reset

[Dmitriy Traytel]

> On 05 Mar 2016, at 23:11, Makarius  wrote:
> 
> *** ML ***
> 
> * Local_Theory.restore has been renamed to Local_Theory.reset to
> emphasize its disruptive impact on the cumulative context, notably the
> scope of 'private' or 'qualified' names. Note that Local_Theory.reset is
> only appropriate when targets are managed, e.g. starting from a global
> theory and returning to it. Regular definitional packages should use
> balanced blocks of Local_Theory.open_target versus
> Local_Theory.close_target instead. Rare INCOMPATIBILITY.
> 
> 
> This refers to Isabelle/aae510e9a698. This changeset also shows that 
> remaining uses of the disruptive Local_Theory.reset are here:
> 
> src/HOL/Library/bnf_axiomatization.ML
> src/HOL/Tools/Lifting/lifting_def.ML
> src/HOL/Tools/Lifting/lifting_def_code_dt.ML
> src/HOL/Tools/Transfer/transfer_bnf.ML

The uses in

src/HOL/Library/bnf_axiomatization.ML
src/HOL/Tools/Transfer/transfer_bnf.ML

are gone in b5d656bf0441. The one in transfer_bnf.ML actually became obsolete 
with change eeaa2f7b5329 (or some of its immediate predecessors)—I somehow 
didn’t think of removing it.

Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Discovering named_theorems

[Dmitriy Traytel]

Hi all,

trying the smaller audience of isabelle-dev first.

I wondered whether named_theorems (or more generally all dynamic facts) deserve 
to be more visible. In particular when I search for

"(?a < ?c - ?b) = (?a + ?b < ?c)”

with find_theorems, I’d like to be reminded of algebra_simps (instead or rather 
in addition to Groups.ordered_ab_group_add_class.less_diff_eq).

Looking at the named_theorems that we have today (with grep), I see two kinds: 
those relevant for the working formalizer (algebra_simps, derivative_intros, 
...), and those mostly relevant for tools (transfer_raw, …). It would be good 
to make the former ones easily discoverable (via find_theorems, potentially 
also Sledgehammer). If something is really irrelevant for the working 
formalizer, it(s binding) could in principle be concealed (preventing 
find_theorems from showing it).

Technically, the Facts module today does not expose functions to query all the 
dynamic facts (mirroring the existing ones for static facts Facts.fold_static 
and Facts.dest_static). Concretely, I’d like to see functions a la

  val fold_dynamic: Context.generic -> (string * thm list -> 'a -> 'a) -> T -> 
'a -> 'a
  val dest_dynamic: Context.generic -> bool -> T list -> T -> (string * thm 
list) list

and maybe also

  val fold: Context.generic -> (bool * string * thm list -> 'a -> 'a) -> T -> 
'a -> 'a
  val dest: Context.generic -> bool -> T list -> T -> (bool * string * thm 
list) list

which combine dynamic and static facts in Facts.

As a second step the querying tools (find_theorems, Sledgehammer, etc.) could 
decide what to show and what not.

Am I overlooking something fundamental, why this should/can not be done?

Dmitriy

PS: The real reason why I am interested in this is that in the forthcoming 
package for non-primitive corecursion (joint work with Jasmin Blanchette, 
Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu), we would like to generate 
dynamic theorems for coinduction up to congruence (because the coinduction 
principles gets stronger with every non-primitively corecursive function 
defined). But this only makes sense if users are aware of those dynamic 
theorems, i.e. can find them easily.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Odd name space problem in quickcheck or codegen (due to change in typedef)

[Dmitriy Traytel]

Maybe a guess in the blue, but here is what grep tells me:

~$ grep base_name ~/isabelle/src/HOL/Tools/ -r | grep Quick
/Users/traytel/isabelle/src/HOL/Tools//Quickcheck/abstract_generators.ML:
val name = Long_Name.base_name tyco

I have not investigated further.

Dmitriy

> On 27 Feb 2016, at 19:36, Makarius  wrote:
> 
> On Sat, 27 Feb 2016, Florian Haftmann wrote:
> 
>> Are you still close enough to obtain an ML traceback?  It will take some 
>> time for me to analyze this.
> 
> The exception trace (produced with polyml-5.3.0) points to 
> src/HOL/Tools/Quickcheck/random_generators.ML: compile_generator_expr_raw / 
> iterate_and_collect. It think it is coming from "compile" defined as 
> Code_Runtime.dynamic_value_strict.
> 
> It is very difficult to figure out where it really happens, due to all these 
> indirections of Random_Engine.run etc.
> 
> 
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Maintenance work on Jenkins VM

[Dmitriy Traytel]

Hi Lars,

even without the slow sessions, this is of great help. Thanks!

My commit yesterday (isabelle/ae44f16dcea5) broke some AFP entries (because 
without the afp_testboard, I used to follow the "break it, fix it” philosophy 
w.r.t. AFP). I will repair those today.

Dmitriy

> On 17 Feb 2016, at 00:22, Lars Hupel  wrote:
> 
> Hi Dmitriy,
> 
>> What about having an additional afp_testboard repository where one 
>> could also push -f changes. I am particularly interested in “slow” 
>> sessions there.
> 
> for now I've created a job which runs everything but the slow sessions
> (so not quite what you wanted). The repository is:
> 
>  
> 
> Same rules as for the Isabelle testboard apply.
> 
> The corresponding job is:
> 
>  
> 
> Cheers
> Lars

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance window

[Dmitriy Traytel]

> On 16 Feb 2016, at 11:30, Makarius <makar...@sketis.net> wrote:
> 
> On Tue, 16 Feb 2016, Dmitriy Traytel wrote:
> 
>> I am unsure if an Isabelle tool is the right level of abstraction for an 
>> operation, only members of the isabelle (UNIX) group at TUM can/should 
>> execute.
> 
> BTW, the Isabelle tool name space is not hardwired. Any "component" can add 
> new tool directories by augmenting ISABELLE_TOOLS.
> 
> So there could be a "testboard" component to abstract whatever needs to be 
> abstracted.

I see. Then I am in favor of a “non-main” component that provides a tool which 
starts a new test job (either via plain push -f as before, or something 
complicated involving new repositories but also supporting mq-patches).

Dmitriy

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance window

[Dmitriy Traytel]

Hi Lars,

I am unsure if an Isabelle tool is the right level of abstraction for an 
operation, only members of the isabelle (UNIX) group at TUM can/should execute.

Also, wouldn’t a push to a fresh repository take quite long. (OK, negligible 
compared to the actual build, but still.) And one still would need to use the 
-f for testing mq-patches.

Overall, I don’t see a too big problem with force-pushing. Florian showed how 
to do it properly on the client's side [1]. If everybody would just use this 
setup, we would not be talking here.

Dmitriy

[1] 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-February/002258.html


> On 16 Feb 2016, at 10:44, Lars Hupel  wrote:
> 
>> Was it me? I think I saw a warning to that effect, but with "-f"
>> (which is necessary since we're creating new heads) it's too late
>> once the warning is shown. I can easily change the trusty old script
>> I use to push to testboard to make sure I do it from my Isabelle
>> repository. If it happens once every five years or so, maybe it's not
>> so great an issue that the workflow needs to be changed.
> 
> As I said, I'm not blaming anybody. Any workflow which requires
> force-pushing on a regular basis is broken. In particular, I wouldn't
> want to encourage contributors to make their own scripts.
> 
> To that end I'm suggesting an official "Isabelle tool" which schedules
> testboard builds. Ideally this would push to some fresh repository,
> schedule a build, and delete the repository again. Users would write
> "isabelle testboard" and be done with it. I'll sit down on the weekend
> and try to come up with a proof of concept.
> 
> Cheers
> Lars
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Maintenance work on Jenkins VM

[Dmitriy Traytel]

Hi Lars,

great to hear!

What about having an additional afp_testboard repository where one could also 
push -f changes. I am particularly interested in “slow” sessions there.

Thanks for your work,
Dmitriy

> On 30 Jan 2016, at 12:51, Lars Hupel  wrote:
> 
> Dear list,
> 
> I'm currently performing maintenance work on the Jenkins VM. The
> following things are planned for today:
> 
> - running makeall and AFP (without "slow" sessions) on every push to
> Isabelle
> - running slow sessions nightly
> - utilize 4 workers (8 cores, 64 GB each) from the LRZ
> 
> I've already tested the above configuration locally and am currently
> applying it to the production CI server.
> 
> If that works out fine, I will additionally deploy the following jobs:
> 
> - running AFP (without "slow" sessions) on every push to AFP
> - running everything on every push to testboard
> 
> Cheers
> Lars
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Update of jdk and jedit components

[Dmitriy Traytel]

Hi Makarius,

here is one way to still (e1e6bb36b27a) edit the output buffer: to use the 
compose key.

On my Mac, if I place the cursor into the output buffer and press alt-u 
followed bei u, an ü appears in the output.

Dmitriy

> On 04 Nov 2015, at 20:42, Makarius  wrote:
> 
> On Wed, 4 Nov 2015, Makarius wrote:
> 
>> This incident means I need to figure out a different way to avoid edits on 
>> output-only text areas.
> 
> See now
> 
> changeset:   61570:f26a4d5e82b5
> user:wenzelm
> date:Wed Nov 04 17:14:17 2015 +0100
> files:   src/Tools/jEdit/src/pretty_text_area.scala
> description:
> dummy input handler to imitate former read-only mode, which has changed its 
> meaning in jedit-5.3.0 as mere hint for saving;
> 
> 
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] copy_bnf

[Dmitriy Traytel]

Hi Lars,

this was exactly the vision for copy_bnf, modulo that I thought of using a 
plugin (“src/Pure/Tools/plugin.ML”) instead of an option. But since I am not 
the author of record, I went for the less invasive option of a separate command 
(in the spirit of setup_lifting for typedef). So if the authors of record 
agree, I can add the plugin.

I guess the general question is, whether it is fine to add the plugin 
infrastructure for (most of the) existing commands (e.g., definition, typedef, 
record, fun), thus enabling us writing tools that extend the command’s 
functionality (be them enabled by default or not).

Dmitriy


> On 29 Oct 2015, at 13:41, Lars Hupel  wrote:
> 
> Dear Dmitriy,
> 
> I like the new "copy_bnf" command a lot, especially to allow records to
> be used in nested recursion. However, after a record definition, I have
> to invoke the command manually*. I would like to propose that "record"
> gains an option to call it directly. So, instead of writing:
> 
>  record 'a foo = bla :: 'a
> 
>  copy_bnf ('a, 'b) foo_ext
> 
> ... I could write
> 
>  record (copy_bnf) 'a foo = bla :: 'a
> 
> Depending on the efficiency of the internal constructions "copy_bnf"
> could also be the default.
> 
> I do have a use case for this: Lem** is able to generate Isar sources
> containing records, and in CakeML, these records are then used for
> nested recursion. Lem could be changed to emit an additional "copy_bnf",
> but that would make it dependent on the internal construction ("_ext").
> Hence, I would much prefer a flag or to run it by default.
> 
> Cheers
> Lars
> 
> 
> * and to remember that I need to use "foo_ext" because otherwise I get
> an ML exception
> 
> ** 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Broken AFP sessions

[Dmitriy Traytel]

Those look to me as if they have to do with 2314c2f62eb1 (real_of_nat_Suc is 
now a simprule). Verified only for the Integral.thy failure.

Dmitriy


> On 06 Oct 2015, at 23:19, Makarius  wrote:
> 
> Here are some more proof failures (Isabelle/5b5656a63bd6 and 
> AFP/21bdf9fbf229):
> 
> Integration FAILED
> *** At command "by" (line 1724 of 
> "~/isabelle/afp-devel/thys/Integration/Integral.thy")
> 
> Markov_Models FAILED
> *** At command "done" (line 1038 of 
> "~/isabelle/afp-devel/thys/Markov_Models/Classifying_Markov_Chain_States.thy")
> *** At command "by" (line 1077 of 
> "~/isabelle/afp-devel/thys/Markov_Models/Classifying_Markov_Chain_States.thy")
> 
> Ordinary_Differential_Equations FAILED
> *** At command "by" (line 804 of 
> "~/isabelle/afp-devel/thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy")
> *** At command "by" (line 704 of 
> "~/isabelle/afp-devel/thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy")
> 
> 
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Proofs broken?

[Dmitriy Traytel]

As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in about 
17 minutes.

Timing = :threads=4elapsed=979.269cpu=2582.077gc=323.518factor=2.64

Dmitriy

> On 06 Oct 2015, at 21:54, Jasmin Blanchette  
> wrote:
> 
> Hi Makarius,
> 
>> My impression is that ebf296fe88d7 (blanchet) causes HOL-Proofs to run out 
>> of resources and fail.  I've made approx. 3 runs in the vicinity -- it 
>> always takes very long.
>> 
>> Is that another failure to do a full "isabelle build -a" before pushing 
>> anything?
> 
> I did "isabelle build -a" but stopped after some time because "HOL-Proofs" 
> diverged. Then I went back to the last repository version and had exactly the 
> same divergence behavior. Testboard is down, and if my 2015 MacBook Pro can't 
> do it, we have a problem, already before ebf296fe88d7.
> 
> Jasmin
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Multiset missing Nitpick_Model.unrep in 2007ea8615a2

[Dmitriy Traytel]

The title says it all.

Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Scrollbar, where are thou?

[Dmitriy Traytel]

Hi,

I’m not sure if this is rather something for the jEdit mailing list, but I try 
here first. The attached theory is an empty 500+ lines long file where 
everything is normal. However, if I add one new line the scrollbar disappears.

The above applies to 2007ea8615a2 but I believe I saw this behaviour already 
weeks (if not months) ago, but didn’t pay attention. In Isabelle2015 everything 
is fine.

Dmitriy



Scratch.thy
Description: Binary data
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Definite name for case combinator on products [was: NEWS]

[Dmitriy Traytel]

Sounds good to me.

Dmitriy

On 22.09.2015 16:20, Florian Haftmann wrote:

So, the direction is going towards prod_case.

If this is settled, the consequences are:
* Abbreviation »uncurry« will disappear again.
* Abbreviation »split« will disappear finally (using the distribution
and AFP as indicator whether this is »now« or »later«).
* Theorem names contain »prod_case« instead of »split«; the latter are
retained as aliasses, but documentation etc. is updated to prefer the
first version.
* There is no way to have something like »curry (uncurry f) = f«
printed; entering »curry (prod_case f) = f« prints as »curry (λ(x, y). f
x y) = f« by default.

Any headache with this?

Florian

Am 10.09.2015 um 12:19 schrieb Dmitriy Traytel:

Hi Florian,

while I very much welcome the simplified printing rules and your effort
of unifying case_prod/split, I am not sure if adding a third alternative
name is the way to go. The situation reminds me of the one depicted in [1].

Clearly, case_prod is the "right" name from the perspective of the
(co)datatype package.

Dmitriy

[1] https://xkcd.com/927/

On 10.09.2015 12:02, Florian Haftmann wrote:

* Combinator to represent case distinction on products is named
"uncurry", with "split" and "prod_case" retained as input abbreviations.

Partially applied occurences of "uncurry" with eta-contracted body
terms are not printed with special syntax, to provide a compact
notation and getting rid of a special-case print translation.

Hence, the "uncurry"-expressions are printed the following way:

a) fully applied "uncurry f p": explicit case-expression;

b) partially applied with explicit double lambda abstraction in
the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;

c) partially applied with eta-contracted body term "uncurry f":
no special syntax, plain "uncurry" combinator.
This aims for maximum readability in a given subterm.
INCOMPATIBILITY.

This refers to e6b1236f9b3d.

This schema emerged after some experimentation and seems to be a
convenient compromise. The longer perspective is to overcome the
case_prod/split schism eventually and consolidate theorem names accordingly.

The next step after this initial cleanup is to tackle the »let (a, b) =
… in …« issue.

Florian



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS

[Dmitriy Traytel]

Hi Florian,

while I very much welcome the simplified printing rules and your effort 
of unifying case_prod/split, I am not sure if adding a third alternative 
name is the way to go. The situation reminds me of the one depicted in [1].


Clearly, case_prod is the "right" name from the perspective of the 
(co)datatype package.


Dmitriy

[1] https://xkcd.com/927/

On 10.09.2015 12:02, Florian Haftmann wrote:

* Combinator to represent case distinction on products is named
"uncurry", with "split" and "prod_case" retained as input abbreviations.

Partially applied occurences of "uncurry" with eta-contracted body
terms are not printed with special syntax, to provide a compact
notation and getting rid of a special-case print translation.

Hence, the "uncurry"-expressions are printed the following way:

a) fully applied "uncurry f p": explicit case-expression;

b) partially applied with explicit double lambda abstraction in
the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;

c) partially applied with eta-contracted body term "uncurry f":
no special syntax, plain "uncurry" combinator.
This aims for maximum readability in a given subterm.
INCOMPATIBILITY.

This refers to e6b1236f9b3d.

This schema emerged after some experimentation and seems to be a
convenient compromise. The longer perspective is to overcome the
case_prod/split schism eventually and consolidate theorem names accordingly.

The next step after this initial cleanup is to tackle the »let (a, b) =
… in …« issue.

Florian



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] testboard

[Dmitriy Traytel]

On 19.08.2015 22:45, Makarius wrote:

On Wed, 19 Aug 2015, Larry Paulson wrote:

I pushed a changeset to the testboard, but it isn’t showing up at 
http://isabelle.in.tum.de/testboard/Isabelle


The last change it shows was 6 days ago.

Moreover, testboard and the default branch look identical (I’m using 
SourceTree), so have I simultaneously pushed my changes to the main 
repository somehow?


Maybe.  The changeset 6a6f15d8fbc4 turned out broken -- I've repaired 
this already in e1159bd15982.


Generally, we are running short of proper test machines -- isatest 
takes very long now.  The fastest machine in reach is the one under my 
desk.



Makarius
I haven't seen the state of the testboard when Larry pushed, but I 
suspect that he pushed to the main repository exclusively (rather than 
simultaneously to the testboard). Note that the testboard requires a 
push -f, otherwise Mercurial will refuse to create a new head.


When I just pushed to the testboard a few minutes ago Mercurial replied with

added 67 changesets with 204 changes to 134 files (+1 heads)

(This is a quite normal response, even though I've added only one 
change, since the testboard is not automatically updated w.r.t. the main 
repository, and I am one of the few people who sometimes pushes to the 
testboard. In effect, I've pushed 67 changes (including Larry's 
changeset 6a6f15d8fbc4) that were pushed to the main repository but not 
to testboard.)


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: isabelle test failed

[Dmitriy Traytel]

Oops, I didn't expect my name to appear here ;-)

The changeset 894d6d863823 was a reaction to Andreas Lochbihler's report 
[1]. With turned off proofs the effect was a good one.


What is special about Pure.conjunction w.r.t. proof reconstruction? Is 
it something in Goal.conjunction_tac? Would you advise to use HOL's 
conjunction instead?


Dmitriy

[1] 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-April/005986.html


On 26.06.2015 20:01, Makarius wrote:

On Fri, 26 Jun 2015, Larry Paulson wrote:

HOL-Proofs, etc., have been failing for several days now. Last time I 
checked, it was simply a timeout. Presumably some change to rewriting 
is to blame. It may be similar to the AFP failure that I fixed 
yesterday. Is anyone familiar with this entry?


I've made some manual tests just yesterday and then produced the 
following change:


changeset:   60574:915da29bf5d9
user:wenzelm
date:Thu Jun 25 22:56:33 2015 +0200
files:   Admin/isatest/settings/at64-poly
description:
more heap -- hoping for more stability of HOL-Proofs;

The isatest from tonight did not see that yet, because I pushed it too 
late after midnight.  Maybe the next test run works.



The deeper reason why HOL-Proofs takes much longer now is this:

The first bad revision is:
changeset:   60046:894d6d863823
user:traytel
date:Mon Apr 13 13:03:41 2015 +0200
summary: call Goal.prove only once for a quadratic number of theorems


I did not find time yet, to look more closely what is behind that.

Generally, proof term performance is bad for massive amounts of goals 
with Pure.conjunction.  I've had a discussion about that around 2008 
with Stefan Berghofer, but he could not explain it, nor improve the 
situation.


More generally, HOL-Proofs always serves as a reminder of invisible 
concrete walls concerning limited CPU resources.  Growth cannot just 
continue forever, one day it will come to a grinding halt. (Despite 
that triviality, I have already some ideas to reduce resource usage 
once again, so that the meltdown might be postponed.)



Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] »real« considered harmful

[Dmitriy Traytel]

I guess what Larry means is there is no way to see a type of a constant 
that is not there in the source.


Consider e.g.

declare [[coercion of_nat :: nat ⇒ real]]
term sqrt (2 :: nat)

Today the output says sqrt (real_of_nat 2). But if there would be no 
abbreviation for of_nat :: nat ⇒ real, how would you deduce the type 
of the coercion.


Dmitriy

On 24.06.2015 16:01, Manuel Eberl wrote:

On 24/06/15 15:55, Larry Paulson wrote:
A more appropriate point is that it can be tricky in Isabelle/jEdit 
to determine the type of an expression such as “of_nat k”, as there 
is nothing to click on.
When I type ‘term sqrt (of_nat 2)’ and hover over the ‘of_nat’, it 
says ‘constant Nat.semiring_1_class.of_nat :: nat ⇒ real’.



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] »real« considered harmful

[Dmitriy Traytel]

You can hover in the output panel, but you won't see types of constants 
there.


Dmitriy

On 24.06.2015 16:09, Manuel Eberl wrote:
Ah, I see the problem. In that case, one could still hover over the 
of_nat in the output window, but it is perhaps not ideal.



On 24/06/15 16:08, Dmitriy Traytel wrote:
I guess what Larry means is there is no way to see a type of a 
constant that is not there in the source.


Consider e.g.

declare [[coercion of_nat :: nat ⇒ real]]
term sqrt (2 :: nat)

Today the output says sqrt (real_of_nat 2). But if there would be 
no abbreviation for of_nat :: nat ⇒ real, how would you deduce the 
type of the coercion.


Dmitriy

On 24.06.2015 16:01, Manuel Eberl wrote:

On 24/06/15 15:55, Larry Paulson wrote:
A more appropriate point is that it can be tricky in Isabelle/jEdit 
to determine the type of an expression such as “of_nat k”, as there 
is nothing to click on.
When I type ‘term sqrt (of_nat 2)’ and hover over the ‘of_nat’, it 
says ‘constant Nat.semiring_1_class.of_nat :: nat ⇒ real’.



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 







___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Dmitriy Traytel]

Hi,

I could not believe that recdef could not be replaced by fun, so here is 
the patch that removes usages of recdef from Decision_Procs. The proof 
rules that come out of the function package are fine (one just needs a 
few split_format (complete) attributes in a few places).


I'm not sure if this is something for the repository though, since it 
has a factor of 2 impact on the build-time:


recdef: Finished HOL-Decision_Procs (0:03:53 elapsed time, 0:13:26 cpu 
time, factor 3.45)
fun   : Finished HOL-Decision_Procs (0:08:24 elapsed time, 0:28:10 cpu 
time, factor 3.35)


On the other hand 8 minutes is still not much. The longest fun 
invocation (numadd in MIR) takes about 2 minutes, other are all below 20 
seconds.


Dmitriy

On 07.06.2015 07:18, Amine Chaieb wrote:
I remember trying to convert Cooper's as well as other Decision proc's 
recdefs to fun, also with the help of Alex but gave up at some point.


I think the killer at the time was rather the induction principle and 
not the simp rules. The one derived by recdef really fits the 
definition and spirit of development. Also runtime at the time was 
not acceptable. I also remember havin the runtime problem with fun vs. 
primrec (so we left those there too).


  Context: Deep embedding of datatype + normal form on this data type 
+ set of recursive functions on syntax preserving normal form. The 
normal Form has conditions on nested patterns -- introduce new 
constructor for these common nested patterns in normal form.


We had combinatorial explosion due to the depth of the patterns (which 
is the main reason to introduce special constructors in the datatype, 
to reduce deep patterns).


The induction priciples with recdef really fitted, i.e. induct auto 
with spice did the job for lemmas you do not expect to spend time 
thinking as a software developer.


One could argue that one should introduce a new data type for 
normalized syntactic elements and perform such computations as needed. 
I dismissed this idea and did not explore it, since it comes with a 
high price. Perhaps there are better ways to do the formalization.


Amine.


On 06/06/2015 08:37 PM, Tobias Nipkow wrote:



On 06/06/2015 20:11, Larry Paulson wrote:
Pattern matching is a convenience, and can always be eliminated 
manually. Is there really no reasonable way to re-express the 
definitions in Cooper.thy?


You can always turn all patterns of the lhs into cases on the rhs and 
derive the individual equations as lemmas. You also need to derive an 
induction principle. I would rather keep recdef than do all that by 
hand.


Tobias


Larry

On 6 Jun 2015, at 16:11, Florian Haftmann 
florian.haftm...@informatik.tu-muenchen.de wrote:



The reason for the continued existence of recdef is that function can
cause a combinatorial explosion the way it compiles pattern 
matches. I
just tried Cooper.thy and changing one of the recdefs to function 
makes
Isabelle go blue (purple) in the face until one gives up. Hardware 
alone

will not solve that one.

Now one could argue that since we need recdef, we should also keep 
the
special variant defer_recdef, but if nobody speaks up for it, we 
don't

have a proof that we really need it and it should go.


At the time of their writing the recdef examples in (nowadays)
src/HOL/Decision_Procs were the power applications of their times.

Since then power applications have grown bigger and bigger and
fun/function have been used widespread.  It seems strange to me 
that no

application since then had never hit the same concrete wall again.

So are there any experience reports that the combinatorial 
explosion in
pattern matching in fun/function had to be worked around somehow?  
Or do

we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed domain-specific?

Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de 



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 







___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


# HG changeset patch
# User traytel
# Date 1433658664 -7200
#  So Jun 07 08:31:04 2015 +0200
# Node ID 03ef7232e0f060ed68756b902bd55ec9a51ed9b7
# Parent  392402362c3e01d9556b59674ce2d4f38903bd0b
get rid of recdef from Decision_Procs

diff -r 392402362c3e -r 03ef7232e0f0 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Fr Jun 05 09:15:37 2015 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	So Jun 07 08:31:04 2015 +0200
@@ -6,7 +6,6 @@
 imports
   Complex_Main
   

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Dmitriy Traytel]

Hi Florian,

On 06.06.2015 17:11, Florian Haftmann wrote:

The reason for the continued existence of recdef is that function can
cause a combinatorial explosion the way it compiles pattern matches. I
just tried Cooper.thy and changing one of the recdefs to function makes
Isabelle go blue (purple) in the face until one gives up. Hardware alone
will not solve that one.

Now one could argue that since we need recdef, we should also keep the
special variant defer_recdef, but if nobody speaks up for it, we don't
have a proof that we really need it and it should go.

At the time of their writing the recdef examples in (nowadays)
src/HOL/Decision_Procs were the power applications of their times.

Since then power applications have grown bigger and bigger and
fun/function have been used widespread.  It seems strange to me that no
application since then had never hit the same concrete wall again.

So are there any experience reports that the combinatorial explosion in
pattern matching in fun/function had to be worked around somehow?  Or do
we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed domain-specific?
I have some experience with the combinatorial explosion in fun. You 
don't need much: just take extended regular expressions (~10 
constructors) and define binary normalizing constructors (by some 
sequential pattern matching on both arguments). The AFP entry 
MSO_Regex_Equivalence is full of ~30 sec fun declarations.


While this is still on the edge of being bearable, try to add one more 
constructor... (I've seen examples where fun from 10 lines of 
specification produced something like 10^5 simp equations.) In a 
different formalization (AFP entry Formula_Derivatives) where I needed 
to have more then 10 constructors, I had to work around the function 
package by separating the datatype into two and defining the functions 
separately. (In the end, the separation had also positive effects, but 
still it felt like fighting the system when doing it.)


Note that the domain is quite similar to Cooper---syntactic 
manipulations of expressions/formulas---but isn't it what we do quite 
often in Isabelle? Orthogonally, I have no idea, whether recdef would 
have helped me.


Dmitriy

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s

[Dmitriy Traytel]

Hi Andreas,

the code plugin defines a new constant (copy of op =) that is used as 
equality.


datatype x = A | B
export_code equal_x_inst.equal_x in SML

To get it executable (#constructors)^2 equations are proved in a 
backward fashion (I'm sure it could be easilly done in a forward fashion 
as well). However, this code goes back to Stefan and Florian, and we 
didn't attempt to optimize it when integrating it with the new package.


But isn't the performance now (894d6d863823 ) already acceptable?

Dmitriy

On 14.04.2015 08:10, Andreas Lochbihler wrote:

Hi Dmitriy,

Thanks for investigating. I am really surprised that the code plugin 
is to blame for the huge overhead. I don't know the details of the 
code plugin, but I have an idea of what it should do: instantiate the 
equals type class, register the constructors as code constructors, and 
declare the pattern-matching equations for case, set, rel, map and 
equals as [code].


None of this should involve any fancy proof. In fact, most of the 
equations should have already been proven by the free_constructors 
part or should be easily derived from them by single-step resolutions. 
What am I missing?


Andreas

On 13/04/15 12:04, Dmitriy Traytel wrote:

Hi Andreas,

I've investigated this a bit and the slowdown happens in the code 
plugin in the
instantiation of the equal type class (i.e. datatype (plugins del: 
code) is more precise
than the advice below). The number of theorems proved there is 
quadratic (8000 in your

case).

But it is still not hopeless: those 8000 theorems are proved one 
after each other calling
Goal.prove for each of them. It is much faster to form the (balanced) 
conjunction, call
Goal.prove (which does among other things type checking) once, and 
then destroy the

conjunction. I'm currently testing this on testboard
(http://isabelle.in.tum.de/testboard/Isabelle/rev/1863cdff2010).

Cheers,
Dmitriy

On 09.04.2015 16:11, Andreas Lochbihler wrote:

Hi Dmitriy and Jasmin,

Thanks for the hint with plugins. That really speeds things up. I 
also suspect that the

timing panel does not include the forked proof tactics.

Cheers,
Andreas

On 09/04/15 15:55, Dmitriy Traytel wrote:

Hi Andreas,

rather than going dirty, try:

datatype (plugins only:) family ...

It seems that here we are lucky and the slowdown is caused by one 
of the plugins. (We'll

investigate which one.)

Cheers,
Dmitriy

PS: Your datatype reminded me of another one, which allows (or 
allowed) proving False in a

different theorem prover ;-)
https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00134.html

On 09.04.2015 15:44, Jasmin Blanchette wrote:

Hi Andreas,

In Isabelle2014, processing this datatype declaration takes about 
one minute. So what
has happened in between? (The Isabelle2014 timing panel is also 
way off with 8 seconds.)
Thanks for your report. What happened in between is that we 
generate more theorems. I
suspect one or a few of them have tactics that scale poorly (e.g. 
cubic) in the number

of constructors.

As for the timing panel, I suspect it does not take into 
consideration the time spent in

tactics with multithreading on, but I’m not an expert there.

We’ll look into this. You could try “quick_and_dirty” around that 
particular datatype to

make things more tolerable in the meantime.

Cheers,

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 







___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s

[Dmitriy Traytel]

Hi Andreas,

I've investigated this a bit and the slowdown happens in the code plugin 
in the instantiation of the equal type class (i.e. datatype (plugins 
del: code) is more precise than the advice below). The number of 
theorems proved there is quadratic (8000 in your case).


But it is still not hopeless: those 8000 theorems are proved one after 
each other calling Goal.prove for each of them. It is much faster to 
form the (balanced) conjunction, call Goal.prove (which does among other 
things type checking) once, and then destroy the conjunction. I'm 
currently testing this on testboard 
(http://isabelle.in.tum.de/testboard/Isabelle/rev/1863cdff2010).


Cheers,
Dmitriy

On 09.04.2015 16:11, Andreas Lochbihler wrote:

Hi Dmitriy and Jasmin,

Thanks for the hint with plugins. That really speeds things up. I also 
suspect that the timing panel does not include the forked proof tactics.


Cheers,
Andreas

On 09/04/15 15:55, Dmitriy Traytel wrote:

Hi Andreas,

rather than going dirty, try:

datatype (plugins only:) family ...

It seems that here we are lucky and the slowdown is caused by one 
of the plugins. (We'll

investigate which one.)

Cheers,
Dmitriy

PS: Your datatype reminded me of another one, which allows (or 
allowed) proving False in a

different theorem prover ;-)
https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00134.html

On 09.04.2015 15:44, Jasmin Blanchette wrote:

Hi Andreas,

In Isabelle2014, processing this datatype declaration takes about 
one minute. So what
has happened in between? (The Isabelle2014 timing panel is also way 
off with 8 seconds.)
Thanks for your report. What happened in between is that we generate 
more theorems. I
suspect one or a few of them have tactics that scale poorly (e.g. 
cubic) in the number

of constructors.

As for the timing panel, I suspect it does not take into 
consideration the time spent in

tactics with multithreading on, but I’m not an expert there.

We’ll look into this. You could try “quick_and_dirty” around that 
particular datatype to

make things more tolerable in the meantime.

Cheers,

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 





___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s

[Dmitriy Traytel]

Hi Andreas,

rather than going dirty, try:

datatype (plugins only:) family ...

It seems that here we are lucky and the slowdown is caused by one of 
the plugins. (We'll investigate which one.)


Cheers,
Dmitriy

PS: Your datatype reminded me of another one, which allows (or allowed) 
proving False in a different theorem prover ;-)

https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00134.html

On 09.04.2015 15:44, Jasmin Blanchette wrote:

Hi Andreas,


In Isabelle2014, processing this datatype declaration takes about one minute. 
So what has happened in between? (The Isabelle2014 timing panel is also way off 
with 8 seconds.)

Thanks for your report. What happened in between is that we generate more 
theorems. I suspect one or a few of them have tactics that scale poorly (e.g. 
cubic) in the number of constructors.

As for the timing panel, I suspect it does not take into consideration the time 
spent in tactics with multithreading on, but I’m not an expert there.

We’ll look into this. You could try “quick_and_dirty” around that particular 
datatype to make things more tolerable in the meantime.

Cheers,

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Local_Theory.open_target instead of Local_Theory.restore

[Dmitriy Traytel]

Hi Makarius,

thanks, this is the hint I was looking for a long time now.

I will do the replacement in the BNF package, but I don't think that I 
will have time for it before the approaching release.


Dmitriy

On 07.04.2015 17:47, Makarius wrote:

Just a short note on Local_Theory.open_target (for Isabelle/83071f4c8ae6)
versus old uses of Local_Theory.restore.

Local_Theory.open_target is the internal version of context begin, 
where Local_Theory.close_target is end.  The ML signature is now a 
bit more concise form than before.  It has already been used 
successfully in Eisbach, to lay out a local situation for the internal 
construction.



Here is a quick example that shows how to get polymorphic constants 
out of local theory specifications, with such official context nesting:


context fixes x :: 'a
begin

declare [[show_types]]
ML_val ‹
  val lthy = @{context};
  val (_, lthy1) = lthy | Local_Theory.open_target;
  val ((t, (_, th)), lthy2) = lthy1
| Local_Theory.define ((@{binding c}, NoSyn), 
(Attrib.empty_binding, @{term λy. x}));

  val lthy3 = lthy2 | Local_Theory.close_target;
  val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of 
lthy3);


  val th' = th | singleton (Proof_Context.export lthy2 lthy3);
  val th'' = th' | singleton (Proof_Context.export lthy3 thy_ctxt);

  writeln (Display.string_of_thm lthy2 th);  (*monomorphic*)
  writeln (Display.string_of_thm lthy3 th');  (*partly polymorphic*)
  writeln (Display.string_of_thm thy_ctxt th'');  (*fully polymorphic*)
›

Thus the brute-force Local_Theory.restore is avoided, which only works 
properly at the boundary of local theory command transactions anyway.



Eliminating Local_Theory.restore is one of these continuous reform 
projects that can be done now or later.  Note that it would also 
achieve better results for private datatype, because 
Local_Theory.restore disrupts the continuity of the naming policy.


It is up to the BNF guys to say if they intend to do something for the 
Isabelle2015 release, or just leave the status quo.  It is unlikely 
that anybody will notice fine points of private datatype definitions 
before the next release after Isabelle2015.



Makarius


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] How to activate/de-activate unifier-trace from ML-level

[Dmitriy Traytel]

Hi Makarius,

On 10.02.2015 18:30, Makarius wrote:

On Tue, 4 Nov 2014, Makarius wrote:

Strange hacks that work around the absence of proper options encumber 
the introduction of them eventually. It is the usual bootstrap 
problem for reforms.


I actually did start some work in the vicinity of resolve_tac with 
proper context recently, but it will require more time to revisit 
really ancient parts of the system, not to say ancient habits.


Here is an update on this pending thread: current 
Isabelle/50b60f501b05 is the main move to proper context for 
resolve_tac etc.  After endless years of preparation to localize the 
majority of Isabelle tools, it turned out a releatively small change.


What remains are slightly odd entry points without context: 
resolve0_tac/rtac, eresolve_tac/etac, dresolve_tac/dtac.  We could 
probably remove them altogether, but there are a lot of remaining uses 
in the new datatype implementation, which I don't want to change myself.


indeed approximately 2/3 of all usages of rtac in the Isabelle 
distribution + AFP are in our BNF tactics (roughly 2000 occurrences).


Adding a context to each of them would make the tactics even harder to 
read/maintain compared to their current state. The only decent way of 
adding the context everywhere would be via some combinators à la


THEN'': (ctxt - int - tactic) * (ctxt - int - tactic) - ctxt - int 
- tactic


assuming that rtac has type thm - ctxt - int - tactic

or reuse the polymorphism of THEN'  and work with an uncurried version 
of rtac: thm - (ctxt, int) - tactic (and other tactics). Needless to 
say that I could do this only locally in the BNF package, but maybe this 
is a general question of how tactics should look like.


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] adhoc overloading: ugly output

[Dmitriy Traytel]

Hi Chris,

I've pushed it to the testboard (and will push it to the repository in 
case of success):


http://isabelle.in.tum.de/testboard/Isabelle/rev/0d7de4d99eac

Cheers,
Dmitriy

On 28.01.2015 09:55, Christian Sternagel wrote:
It is amazing how easy some things get when a wizard is looking over 
your shoulder (thanks Florian!). It turns out that adhoc overloading 
(which is in essence very similar to abbreviations) did not observe 
some conventions that are followed by the abbreviation command.


By peeking into the sources - even without understanding much of it ;) 
- it can be seen that the flag abbrev_mode is checked for 
abbreviations. By doing the same inside adhoc_overloading the ugly 
output I presented earlier, turned into beautiful symbols.


Could one of the developers be so kind to apply the attached (mq) 
patch (after testing it of course) ;) ?


cheers

chris

On 01/16/2015 02:40 PM, Christian Sternagel wrote:

Here is a related thread


https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04950.html 




which was originated by myself ;) (how embarassing).

cheers

chris

On 01/16/2015 02:35 PM, Christian Sternagel wrote:

Dear all,

in Isabelle2014 as well as c7f6f01ede15 I noticed that the output when
using adhoc overloading together with abbreviations is not optimal
(maybe this was already discovered before but I forgot about it). Now,
it turns out that the same issue (at least superficially it's the same,
but maybe caused by different reasons) arises also for definitions in
local theory contexts (or are those the same as mere abbreviations?).

Let me illustrate what I'm talking about by the following example:

theory Foo
imports
   Main
   ~~/src/Tools/Adhoc_Overloading
begin

consts SHARP :: 'a ⇒ 'b (♯)

context
   fixes shp :: 'a ⇒ 'a
begin

adhoc_overloading
   SHARP shp

definition le_sharp (infix ≤⇩♯ 50)
where
   xs ≤⇩♯ ys ≡ list_all2 (λx y. y = x ∨ y = ♯ x) xs ys

term xs ≤⇩♯ ys
text ‹
   Result in @{term Foo.le_sharp ♯ xs ys} instead of
   more desirable @{term xs ≤⇩♯ ys}. (The same happens
   when we turn the above definition into an abbreviation.)
›

end

text ‹
   In the global theory this also happens, but only for
   abbreviations, not for definitions.
›

definition shp = id

adhoc_overloading SHARP shp

definition le_sharp' (infix ≤⇩♯ 50)
where
   xs ≤⇩♯ ys ≡ list_all2 (λx y. y = x ∨ y = ♯ x) xs ys

term xs ≤⇩♯ ys

end

Unfortunately, at the moment I do not have time to look into adhoc
overloading myself, but let this thread be a reminder. If anybody else
can provide explanations/comments/solutions, please go ahead!

cheers

chris



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading

[Dmitriy Traytel]

Cf. http://isabelle.in.tum.de/testboard/Isabelle/rev/fd70d029af7e

Dmitriy

On 23.11.2014 21:20, Christian Sternagel wrote:

*Moved from isabelle-users*

Thanks for the crucial hint Dmitriy!

Coming back to the original issue of Andreas, some explanation might 
be in order.


What we did until now in adhoc_overloading.ML (more precisely, the 
function insert_variants) was to check for a given constant c of 
type T whether there is a registered variant v whose type unifies 
with T. If so, v was inserted (but with all type-annotations 
flattened to dummyT). After that we just hoped that type-inference 
would do the trick. Apparently this worked quite well in many 
situations (or maybe there are just not that many users of 
adhoc_overloading ;)).


Be that as it may. In Andreas' example this flattening of types 
leads to somewhat unexpected results. Funnily (or maybe it was to be 
expected but I don't know the details) everything worked out in 
top-level thoeries. Somehow types are more polymorphic there (even 
though HOL is not polymorphic at all ;)). With notepad and a fixed 
type 'b the problem occurred (and I guess the same would happen with 
locales).


(I'm not sure whether the TYPE_MATCH exception, which is not raised 
inside adhoc_overloading.ML but caused by its result, is the best 
problem-indicator for users here. Maybe there is also space for 
improvement elsewhere. Comments?)


Anyway, attached is the following series of patches (to be applied in 
this order):


delete - fixes a typo
drop_semicolons - drops semicolons
inst_unifier - uses the obtained unifier to instantiate the type of v
tune - misc tuning

With those applied (the important one is inst_unifier) 
insert_variants does the following. For a given constant c of type 
T, check whether there is a variant v of type T' such that T and 
T' unify. If so, apply the obtained type-unifier to v and insert the 
result instead of c.


I hope this resolves your problem Andreas.

I tested the change on one of my local files that make heavy use of 
adhoc overloading. Maybe someone could have a look, push the changes 
to a test server, and push them to the main repo if everything is fine?


cheers

chris

On 11/23/2014 11:42 AM, Dmitriy Traytel wrote:

Hi Christian,

just a few weeks ago, I learned that Envir.subst_term_types is indeed
the wrong function when substituting with a unifier (instead it is
intended for matchers).

The right functions for unifiers in envir.ML are the ones prefixed with
norm.

Hope that helps,
Dmitriy

On 22.11.2014 21:02, Christian Sternagel wrote:

I'm currently a bit confused by the result of Sign.typ_unify (or
rather the result of applying the corresponding unifier). So maybe
the problem stems from my ignorance w.r.t. to its intended result.

After applying the attached debug patch for the following

  consts pure :: 'a ⇒ 'b

  definition pure_stream :: 'a ⇒ 'a stream
  where pure_stream = sconst

  adhoc_overloading pure pure_stream

  consts ap_stream :: ('a ⇒ 'b) stream ⇒ 'a stream ⇒ 'b stream
(infixl ◇ 70)
  consts S_stream :: (('a ⇒ 'b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'c) stream

  declare [[show_variants]]

  term pure id :: ('b ⇒ 'b) stream

we obtain the output

oconst type: (??'a ⇒ ??'a) ⇒ ('b ⇒ 'b) stream
variant type: ?'a ⇒ ?'a stream
(unifier:,
 {(('a, 0), ([HOL.type], ??'a ⇒ ??'a)),
   ((?'a, 0),
 ([HOL.type],
  'b))}) (line 165 of
/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML)
(candidate term:,
 Const (Scratch.pure_stream,
?'a
 ⇒ ?'a Stream.stream)) (line 167 of
/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML)
(after unification:,
 Const (Scratch.pure_stream,
(??'a ⇒ ??'a)
 ⇒ (??'a
 ⇒ ??'a) Stream.stream)) (line 168 of
/home/griff/Repos/isabelle/src/Tools/adhoc_overloading.ML)
pure_stream id
  :: ('a ⇒ 'a) stream

The result of unification is a bit surprising to me, since the
obtained unifier seems to claim that

  ('b = 'b) = ('b = 'b) stream

and

  (??'a = ??'a) = (??'a = ??'a) stream

are equal. What am I missing here? Maybe Envir.subst_term_types is not
the way to apply the typenv obtained by typ_unify? (In this special
case, if I would call subst_term_types twice with the same typenv, the
result would be as I expected.)

cheers

chris

Btw: the delete patch (which is to be applied before debug) fixes
a typo in the description of no_adhoc_overloading. It is entirely
unrelated to the issue at hand, but maybe somebody could apply it 
anyway.


On 11/21/2014 07:31 PM, Christian Sternagel wrote:

Dear Andreas,

Thanks for the report, I'll have a look. First an immediate 
observation:


When adding the following to Scratch.thy

declare [[show_variants]]

notepad
begin
   fix f :: ('b ⇒ 'b ⇒ 'a) stream
   and x :: 'b stream
   term pure id :: ('b = 'b) stream

the first term results in

pure_stream id
   :: ('c ⇒ 'c) stream

while the second results in

pure_stream id
   :: ('b ⇒ 'b) stream

So it is not surprising that the first causes

Re: [isabelle-dev] BNF: dead or alive?

[Dmitriy Traytel]

Hi Christian,

On 21.11.2014 14:09, Christian Sternagel wrote:

Dear list,

sorry for the subject ;)

René and I are currently at adapting the Show(_Generator) entry of the 
AFP to the new datatype package. And again we stumbled across some 
difficulties we already encountered when adapting the Order_Generator 
(and which are not resolved yet).


I think it best to first demonstrate what I intend to achieve and why 
our recipe looks as it does. So please bear with me.


The goal is, for a given datatype, say 'a list, to automatically 
generate a show-function, i.e., of type


(nat = 'a = shows) = nat = 'a list = shows

that can be used to convert lists into a string-representation (where 
shows is an abbreviation for string = string and the additional 
nat argument is there to indicate whether the result should be 
parenthesized).


Moreover this construction should work via plain 'primrec' (since 
otherwise the jungle of cong-rules and set-simps that looms ahead is 
too daunting). Lets come back to lists:


primrec showsp_list :: ('a = nat = shows) = nat = 'a list = shows
where
  showsp_list s p Nil = shows_string ''Nil'' |
  showsp_list s p (Cons x xs) =
shows_pl p o shows_string ''Cons'' o shows_space o
  s 1 x o shows_space o
  showsp_list s 1 xs o
shows_pr p

Well, this works fine. Now a slightly more complex datatype

datatype 'a tree = Tree 'a 'a tree list

and its show-function:

primrec showsp_tree :: (nat ⇒ 'a ⇒ shows) ⇒ nat ⇒ 'a tree ⇒ shows
where
  showsp_tree s p (Tree x y) =
shows_pl p o shows_string ''Tree'' o shows_space o
  showsp_list (showsp_tree s) 1 y o
shows_pr p

But wait a minute. This results in:

primrec error:
  Invalid map function in showsp_list (showsp_tree s) 1

Which is the reason for doing everything a little bit different. 
Namely, we start with show-functions that assume that all type 
parameters where already replaced by shows (we call them partial 
show-functions, because parts of their argument are already turned 
into shows). Then the above turns into:


primrec pshowsp_list :: nat ⇒ shows list ⇒ shows
where
  pshowsp_list p Nil = shows_string ''Nil'' |
  pshowsp_list p (Cons x xs) =
shows_pl p o shows_string ''Cons'' o shows_space o
  x o shows_space o
  pshowsp_list 1 xs o
shows_pr p

primrec pshowsp_tree :: nat ⇒ shows tree ⇒ shows
where
  pshowsp_tree p (Tree x y) =
shows_pl p o shows_string ''Tree'' o shows_space o
  pshowsp_list 1 (map (pshowsp_tree 1) y) o
shows_pr p

And we obtain our originally desired functions by

definition showsp_list s p xs = pshowsp_list p (map (s 1) xs)
definition showsp_tree s p t = pshowsp_tree p (map_tree (s 1) t)

Looks reasonable so far.



This seems to work pretty well as long as there are no dead type 
parameters involved. *HOWEVER*, how should we go about turning some 
datatype (dead 'a, 'b) dt into (shows, shows) dt if their is no 
way of mapping the 'a?


In general, why not create map-functions that allow to map over *all* 
type parameters. (As I understand it, this was done just a few month 
ago. What where the reasons for the change?).
There was no change, our map functions always have ignored the dead 
parameters. You are confusing this with phantom variables (which used to 
be dead, but are now live, e.g. in datatype 'a ref = Ref addr from 
Imperative_HOL)


When we last brought up this point, Dmitriy suggested that users that 
use dead in their datatypes know what they are doing and that it is 
not a problem when packages break on such types. However, in IsaFoR 
we sometimes kill type parameters just because otherwise the (huge) 
datatype declaration would take to much resources (in terms of memory 
and time). Still, there is no compelling reason (as far as I see) to 
not having compare- and/or show-functions for those types. Wouldn't it 
be generally useful to always have total map-functions (and 
appropriately plug in ids in the internal BNF constructions)?.

Let me cite the relevant part of my email that you refer to.

On 13.11.2014 15:40, Dmitriy Traytel wrote:
I would not care too much about such dead annotations. If a user made 
a variable dead explicitly, she might be aware that this has some 
disadvantages, so it is ok for some automatic tool to refuse working.


A more interesting question is if you can/want to handle datatypes 
where the dead variable naturally arises, e.g., trees nested through 
functions:


datatype ('a, 'b) tree = Node 'a 'b = ('a, 'b) tree

under the assumption that you have the map function for tree which 
would be contravariant in 'b, i.e. of type ('a = 'c) = ('d = 'b) 
= ('a, 'b) tree = ('c, 'd) tree. If the answer to this question is 
yes, then BNF's indeed don't quite capture the right notion of maps 
for you, and you might want to resort to the database collected by the 
functor command. If the answer is no, this means that you do care 
about the (truly) dead variables.
Now, that I see your concrete application, I believe

Re: [isabelle-dev] BNF: dead or alive?

[Dmitriy Traytel]

On 21.11.2014 15:00, Christian Sternagel wrote:

Hi Dmitriy,

thanks for another round of clarification (I should really reread old 
emails before referring to them).


On 11/21/2014 02:43 PM, Dmitriy Traytel wrote:

In general, why not create map-functions that allow to map over *all*
type parameters. (As I understand it, this was done just a few month
ago. What where the reasons for the change?).

There was no change, our map functions always have ignored the dead
parameters. You are confusing this with phantom variables (which used to
be dead, but are now live, e.g. in datatype 'a ref = Ref addr from
Imperative_HOL)


You are right of course. Sorry for the confusion!


When we last brought up this point, Dmitriy suggested that users that
use dead in their datatypes know what they are doing and that it is
not a problem when packages break on such types. However, in IsaFoR
we sometimes kill type parameters just because otherwise the (huge)
datatype declaration would take to much resources (in terms of memory
and time). Still, there is no compelling reason (as far as I see) to
not having compare- and/or show-functions for those types. Wouldn't it
be generally useful to always have total map-functions (and
appropriately plug in ids in the internal BNF constructions)?.

Let me cite the relevant part of my email that you refer to.

On 13.11.2014 15:40, Dmitriy Traytel wrote:

I would not care too much about such dead annotations. If a user made
a variable dead explicitly, she might be aware that this has some
disadvantages, so it is ok for some automatic tool to refuse working.

A more interesting question is if you can/want to handle datatypes
where the dead variable naturally arises, e.g., trees nested through
functions:

Now, that I see your concrete application, I believe the answer to my
question is no. I.e. (show, show) tree is not an instance of show
(just as(show, show) fun is not). This means that you do care about
the dead parameters!

When you use the dead annotation for efficiency, guess where the
efficiency comes from---it comes mainly from not generating set
functions, generating a smaller map-function, and proving no (or less)
theorems about them.


Alas, no free lunch :)

I conclude that in our situation (i.e., comparators and 
show-functions) it is natural to not support datatypes with dead type 
parameters. Would you agree?

Yes.

Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] is_concealed

[Dmitriy Traytel]

Sorry for reviving an ancient thread, but have the constants defined by 
inductive ever been visible to find_consts since Florian's commit (I 
presume 4a3747517552 ?).


Today in be4a911aca71 (but also in Isabelle2014 and even in 
Isabelle2012) in the following


inductive xyz :: bool where xyz
find_consts name: xyz
ML ‹Consts.is_concealed (Sign.consts_of @{theory}) @{const_name xyz}›

find_consts says found nothing and Consts.is_concealed says true.

Visibility of constants is of course also important beyond find_consts, 
e.g. for auto-completion.


Dmitriy

On 09.09.2010 09:57, Florian Haftmann wrote:

Am 09.09.2010 09:15, schrieb Florian Haftmann:

Am 09.09.2010 09:02, schrieb Tobias Nipkow:

Lars noticed an anomaly and Gerwin tracked it down:
Command find_consts searches only for `visible' constants. Those defined
by primrec and fun are visible, but those defined by inductive(_set) are
concealed. It seems that the latter should be visible, too, right? If
so, can somebody close to inductive fix that?

Pushed.

Florian



___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] HOL broken?

[Dmitriy Traytel]

http://isabelle.in.tum.de/reports/Isabelle/report/60d6105dac94411c8f55ea7626a15c71

anybody taking care of this?

Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL/Number_Theory/Primes

[Dmitriy Traytel]

This is in Isabelle2014. In 229765cc3414 I make the same measurements as 
Larry. So indeed (as the text above those lemmas suggests) there seems 
to be a regression with the simplifier setup.


Dmitriy

On 07.11.2014 15:10, Julian Brunner wrote:

The proof that 97 is prime only takes 1.3s on my machine (2.7 GHz i7),
with the whole theory Primes loading in about 4 seconds.

On Wed, Nov 5, 2014 at 8:37 PM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:

This theory takes quite a while to load, and I have found out why:

text{* A bit of regression testing: *}

lemma prime(97::nat) by simp
lemma prime(997::nat) by eval

The proof that 97 is prime takes 35 seconds on a very fast machine. Can we get 
rid of this or at least substitute a smaller number?

The question is whether this has really to be performed using simp.

As an alternative, a suitable code equations could be proven using the
primes_upto in Eratosthenes.thy, but I did never take any measurements
at which threshold the additional data structures outperform brute-force
calculation.

 Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL/Number_Theory/Primes

[Dmitriy Traytel]

The culprit seems to be dvd_imp_mod_0 introduced as a simp rule in 
773b378d9313.


The following takes again only 2 seconds.

declare dvd_imp_mod_0[simp del]
lemma prime(97::nat) by simp

Dmitriy

On 07.11.2014 15:31, Tobias Nipkow wrote:
Very nice observations, thank you. I was obviously too hasty to remove 
the test which exposed this time leak. Once this issue has been fixed, 
I will put the long test back in, with a better comment.


Tobias

On 07/11/2014 15:27, Dmitriy Traytel wrote:
This is in Isabelle2014. In 229765cc3414 I make the same measurements 
as Larry.

So indeed (as the text above those lemmas suggests) there seems to be a
regression with the simplifier setup.

Dmitriy

On 07.11.2014 15:10, Julian Brunner wrote:

The proof that 97 is prime only takes 1.3s on my machine (2.7 GHz i7),
with the whole theory Primes loading in about 4 seconds.

On Wed, Nov 5, 2014 at 8:37 PM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:

This theory takes quite a while to load, and I have found out why:

text{* A bit of regression testing: *}

lemma prime(97::nat) by simp
lemma prime(997::nat) by eval

The proof that 97 is prime takes 35 seconds on a very fast 
machine. Can we

get rid of this or at least substitute a smaller number?

The question is whether this has really to be performed using simp.

As an alternative, a suitable code equations could be proven using the
primes_upto in Eratosthenes.thy, but I did never take any measurements
at which threshold the additional data structures outperform 
brute-force

calculation.

 Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de 





___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 




___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 





___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Problem in the AFP

[Dmitriy Traytel]

Yes, that's my bad. Thanks! I was about to check Mira for complaints. 
See now AFP/ 1dd93cc85dfb.


Dmitriy

On 23.10.2014 14:25, Florian Haftmann wrote:

Isabelle 06dfbfa4b3ea
AFP 33c18a9138e9

*** Unknown old-style datatype Regular_Exp.rexp
*** At command derive (line 18 of
/mnt/home/haftmann/data/afp/devel/thys/Containers/Compatibility_Containers_Regular_Sets.thy)

Florian



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Datatypes Isatest failures

[Dmitriy Traytel]

On 17.09.2014 11:40, Jasmin Christian Blanchette wrote:

There are only a handful of old_datatypes left in the AFP, and they will go 
away as soon as Dmitriy gets a chance to fix a bug in his code (presumably once he's back 
from vacation).
It is now (isabelle/7b92932ffea5) fixed, and the old_datatypes are 
gone from the AFP (AFP/5bda5332b484).


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] default cases rule

[Dmitriy Traytel]

Hi Chris,

Am 05.09.2014 um 12:27 schrieb Christian Sternagel:

[...]

First question: is this intentional and what is the current default rule?

Yes. Quoting from the news:


The rule set_cases is now registered with the [cases set]
attribute. This can influence the behavior of the cases proof
method when more than one case rule is applicable (e.g., an
assumption is of the form w : set ws and the method cases w
is invoked). The solution is to specify the case rule explicitly
(e.g. cases w rule: widget.exhaust).
INCOMPATIBILITY.



Second question: is it considered bad form to rely on default rules?
No, I think it's fine. Such (radical) changes of definitions (set in 
this case) are seldom.


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Problems with datatype-new

[Dmitriy Traytel]

Hi René,

this is a tactic failure in the recent size extension (the interface 
with fun). We will work on it.


Thanks for the report,
Dmitriy

On 25.06.2014 13:49, René Thiemann wrote:

Dear all,

I have an unexpected problem when defining a datatype using datatype_new.

theory Test
imports
   $AFP/Collections/ICF/impl/RBTSetImpl
begin
datatype_new ('a,'b) bar = Foo 'a 'b option 'b rs

(*
Proof failed.
  1. ⋀g ga h.
local.bar.ctor_rec_bar
 (λx. case local.bar.Rep_bar_pre_bar x of (l, la, xa) ⇒ h (g l) 
(map_option (λx. x) la) xa) =
local.bar.ctor_rec_bar (λx. case local.bar.Rep_bar_pre_bar x of (x1, 
xa, xb) ⇒ h (g x1) xa xb)
The error(s) above occurred for the goal statement⌂:
⋀g ga h. local.bar.rec_bar h ∘ local.bar.map_bar g = local.bar.rec_bar (λx. h 
(g x))*)
end

The problem vanishes if I make the datatype slightly more easier, e.g., if
- I declare 'a or 'b as dead
- 'b option or 'b rs is changed to pure 'b
- 'a is dropped

Just wanting to report this,
René

Isabelle: 52dfde98be4a
AFP: 23c1c5591d9f
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Fwd: [isabelle] New AFP entry: Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions

[Dmitriy Traytel]

I'm following the suggestion of announcing who will fix a new AFP entry 
for the development version.


Of course, I will take care of MSO_Regex_Equivalence once it is merged 
into the development branch. The patch is actually already prepared.


Dmitriy


 Original-Nachricht 
Betreff: 	[isabelle] New AFP entry: Decision Procedures for MSO on Words 
Based on Derivatives of Regular Expressions

Datum:  Thu, 12 Jun 2014 22:35:58 +0200
Von:Tobias Nipkow nip...@in.tum.de
An: Isabelle Users isabelle-us...@cl.cam.ac.uk



Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Dmitriy Traytel and Tobias Nipkow

Monadic second-order logic on finite words (MSO) is a decidable yet expressive
logic into which many decision problems can be encoded. Since MSO formulas
correspond to regular languages, equivalence of MSO formulas can be reduced to
the equivalence of some regular structures (e.g. automata). We verify an
executable decision procedure for MSO formulas that is not based on automata but
on regular expressions.

Decision procedures for regular expression equivalence have been formalized
before, usually based on Brzozowski derivatives. Yet, for a straightforward
embedding of MSO formulas into regular expressions an extension of regular
expressions with a projection operation is required. We prove total correctness
and completeness of an equivalence checker for regular expressions extended in
that way. We also define a language-preserving translation of formulas into
regular expressions with respect to two different semantics of MSO.

The formalization is described in this ICFP 2013 functional pearl:
http://www21.in.tum.de/~nipkow/pubs/icfp13.html

http://afp.sourceforge.net/entries/MSO_Regex_Equivalence.shtml

Enjoy!



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Notes on datatype_new list

[Dmitriy Traytel]

Am 26.05.2014 11:07, schrieb Jasmin Blanchette:

Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de:


The definition of list should look like before.

I don't see how this is an option. This would result in the following duplicate 
constants:

 map_list vs. map
 set_list vs. set
 rel_list vs. forall_list2
 un_Cons1 vs. hd
 un_Cons2 vs. tl
Here are some compromise options that lighten the presentation, but 
still reusing the conveniences provided by the package (which are not 
only the constants, but also many theorems about the constants):


(a)

datatype_new 'a list =
Nil (defaults un_Cons2: []) ([])
| Cons 'a 'a list (infixr # 65)

abbreviation map ≡ map_list
abbreviation set ≡ set_list
abbreviation list_all2 ≡ rel_list
abbreviation hd ≡ un_Cons1
abbreviation tl ≡ un_Cons2

(b)

datatype_new 'a list =
Nil (defaults tl: []) ([])
| Cons (hd: 'a) (tl: 'a list) (infixr # 65)

abbreviation map ≡ map_list
abbreviation set ≡ set_list
abbreviation list_all2 ≡ rel_list

Option (a) is closest to the original definition---the only difference 
is in the annotation defining the default value of tl Nil. However, 
not using the selector requires us to use the automatically generated 
name un_Cons2, which makes this option too obscure.


My favourite (next to the current definition from the repository) is 
option (b)---giving name to the selectors makes the defaults 
annotation easy to parse. And even major functional programming 
languages support similar selector annotations (e.g. via record syntax 
for data in Haskell).


For both options we probably would change the package to generate the 
discriminator %x. x = Nil by default for nullary constructors.


Dmitriy


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Notes on datatype_new list

[Dmitriy Traytel]

Am 26.05.2014 11:46, schrieb Tobias Nipkow:


On 26/05/2014 11:07, Jasmin Blanchette wrote:

Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de:


The definition of list should look like before.

I don't see how this is an option. This would result in the following duplicate 
constants:

 map_list vs. map
 set_list vs. set
 rel_list vs. forall_list2
 un_Cons1 vs. hd
 un_Cons2 vs. tl

Duplicate constants are not a killer argument per se. But why not generate those
constants only if the definer asks for them explicitly?
Let's distinguish between A = {hd, tl} and B = {map, set, rel}. The 
constants from B are an integral part of the package---they form 
together with the type a BNF. Thus, they will always be generated. The 
question is whether they are exposed to the user.


The selectors (A) indeed belong in the category of syntactic sugar, and 
we have an option to not generate those constants. Here, the question is 
about the default behaviour.



  Does any programming
language give you all of them by default? Have you made a study of existing
Isabelle datatypes to see how frequently people defined their own
map/set/rel/selectors?
We did not make a global study. But let me pick a random example 'a 
rexp from your Regular_Set AFP entry. The theory used to define both 
the set function (for atoms) and the map function (for generating marked 
regular expressions IIRC). Defining those functions are essentially 
boring bureaucracy (each taking 7 lines, not to mention the theorems one 
needs to prove about them). In the development version of the AFP, I 
changed those to be generated by the new package, saving some lines of 
code and allowing the reader to focus on more interesting constants.


The relator is in my experience slightly less user-relevant but it 
constitutes an important bridge to the Lifting and Transfer tools.


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Notes on datatype_new list

[Dmitriy Traytel]

Am 26.05.2014 12:25, schrieb Makarius:

On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:

The = as the name for Nil's discriminator deserves an explanation. 
[...] So I introduced this weird = syntax, which suggests that 
equality is used for discriminating. I am open to other suggestions.


The other funky syntax we have is -:. E.g.

   datatype_new (-: 'a) list = ...

This says: Don't generate a set function for 'a -- and don't allow 
nesting through lists.


Just on the squiggles in isolation: if these are rare add-on options 
one could invent long / explicit keywords for them (or Parse.literal 
items).


grep gives 371 occurences of -: in IsaFoR's development repository. So 
it's not a rare add-on, but an important performance optimization.


Dmitriy

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Notes on datatype_new list

[Dmitriy Traytel]

Am 26.05.2014 12:53, schrieb Makarius:

On Mon, 26 May 2014, Dmitriy Traytel wrote:

 Just on the squiggles in isolation: if these are rare add-on 
options one
 could invent long / explicit keywords for them (or Parse.literal 
items).


grep gives 371 occurences of -: in IsaFoR's development repository. 
So it's not a rare add-on, but an important performance optimization.


If it is only an optimization it is conceptually still rare. But of 
course it is also possible to invent short keywords -- after some 
empricial studies about the danger of clashing with common identifiers.


The datatypes manual calls the above dead so that is an obvious 
choice to try out.


Yes, we have considered this naming earlier. It was discarded, because 
it looks like one is giving the name dead to a set function. The same 
holds for any other identifier (not only the common ones). That was the 
reason to use something that is not an identifier.


Dmitriy

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] bnf_decl axiomatization

[Dmitriy Traytel]

Am 13.05.2014 08:09, schrieb Jasmin Christian Blanchette:

Am 12.05.2014 um 23:10 schrieb Makarius makar...@sketis.net:


This sounds both a bit like testing-unstable-HOL.  But there is no problem to 
experiment with axiomatizations, if it clear to the user what it is, and not a seamingly harmless 
bnf_decl.

For the record: The name bnf_decl was modeled after typedecl, since they provide 
similar services. But now that you point it out, I agree that the axiomatic component of bnf_decl 
should be emphasized.


So why not just call it 'bnf_axiomatization' following the recent naming trend?

That's a nice name. Dmitriy, let's go for it. ;)


Cf. 5fff4dc31d34.

Let me explain Jasmin's ;): bnf_axiomatization was the name, I 
intended for the command first, before I was persuaded by my colleagues 
to correlate the name with typedecl rather than axiomatization.


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] bnf_decl axiomatization

[Dmitriy Traytel]

Am 12.05.2014 16:54, schrieb Makarius:
This is a continuation of the thread: code_pred introduces axioms? 
(October / November 2013).


Back then, on Thu, 31 Oct 2013, Andreas Lochbihler wrote:

When Lukas told me about the axioms about three years ago, he said 
that indeed these axioms only specify new constants which the 
inductify option of code_pred introduces for code generation. He 
wanted to somewhen implement proper definitions for these constants, 
but never found the time.


Axioms that only specify new constants are of course an euphemism.  
It is the nature of axiomatization that the slightest mistake, either 
conceptually on paper or in the implementation, destroys the whole 
logical environment.


After the above incident, I looked around systematically for more such 
surprises in main HOL or its libraries.


A remanining item on the list is 'bnd_decl'.  How does that fit in the 
picture?  Why have an axiomatic version of something that has been 
properly founded on top of existing Isabelle/HOL in a purely 
definitional manner?



Just syntactically, anything that is axiomatic should be clearly 
visible as such, to avoid the surprise when a user thinks to switch on 
the light, but has in fact pushed the nuke button.


Hi Makarius,

the bnf_decl command declares a new type together with its BNF structure
and automatizes the BNF properties. I've put it in HOL/Library only from 
the start,

because of its axiomatic nature.

There are two classes of users for bnf_decl:

the Popescu-class:
  Anybody who would like to be able to quantify over type constructors
  in HOL in order to reason abstractly. The command bnf_decl is a first
  approximation of this: one can directly formalize statements like
  for all bounded natural functors F have  Of course this 
quantification

  happens only on a meta level---no instantiation of the quantifier is
  possible (without trying to resurrect the AWE tool). One example of such
  a formalization is in src/HOL/BNF_Examples/Stream_Processor which
  follows [1, p9, Remark].

the Traytel-class:
  Any developer of extensions to the BNF machinery. Here the axiomatic
  command provides the abstract example with which we usually test our
  proof tactics---cf. the formalization of the BNF operations [2]
  associated with our ITP 2014 paper.

Of course, it is relatively easy to construct not-so-abstract examples of
BNFs using the concrete, definitional datatype_new declaration (and
pretending to forget the definition afterwards). Thus, it would not be a
huge problem for the Traytel-class if the command would disappear (in
this case I'm less sure about an adequate replacement for the 
Popescu-class.)

or be moved elsewhere (potentially to the AFP?).

Dmitriy

[1] https://personal.cis.strath.ac.uk/neil.ghani/papers/ghani-lmcs09.pdf
[2] http://www21.in.tum.de/~blanchet/codata_impl.tar.gz

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] status (AFP)

[Dmitriy Traytel]

Could it be the document preparation?

Dmitriy

Am 05.05.2014 11:17, schrieb Johannes Hölzl:

Has anybody an idea why the AFP test for Probabilistic_Noninterference
fails?

When I build it on my machine with either the combination in the email
(i.e. AFP acd2cc051b4f and Isabelle 52e5bf245b2a) or a recent hg version
(AFP a0a65428715f and Isabelle d940ad3959c5) it works without problems.

  - Johannes

Am Montag, den 05.05.2014, 07:50 +0200 schrieb Isabelle :

The status of the following AFP entries changed or remains FAIL:
[Selection_Heap_Sort] is still on FAIL.
[Native_Word] is still on FAIL.
[HyperCTL] is still on FAIL.
[Launchbury] is still on FAIL.
[Probabilistic_Noninterference] is still on FAIL.

Full entry status at http://afp.sourceforge.net/status.shtml

AFP version: development -- hg id acd2cc051b4f
Isabelle version: devel -- hg id 52e5bf245b2a
Test ended on: macbroy2, Mon May  5 07:50:12 CEST 2014.

Have a nice day,
   isatest



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: improved support for Isabelle/ML

[Dmitriy Traytel]

Am 31.03.2014 23:14, schrieb Makarius:

On Fri, 28 Feb 2014, Makarius wrote:

I've made another round of refinements (presently at 
Isabelle/f7ceebe2f1b5). There were some situations where the change 
propagation of blobs (auxiliary files) versus theories was not right, 
leading to an invalid perspective of the latter, and causing it to be 
rechecked to the bottom whenever it lost its physical editor view. 
This and some other fine points are now sorted out.


Note that the basic model is this: auxiliary files are either managed 
by the editor (via document updates) or the prover (via file-system 
access). If that status changes, e.g. by opening or closing some ML 
file in the editor, the corresponding thy_load command (e.g. 
'ML_file') is updated, and the theories rechecked from that point 
(according to their own perspective, not the whole text as before).  
Anything apart from that is probably a mistake.


I could try harder to manage files always from the editor side, as 
done for theories, but then we hit the performance problems reported 
below ...


Here are again some refinements towards scalable Isabelle/ML IDE 
support (presently Isabelle/075397022503):


  * ML_file references are *not* resolved by default as before, mainly 
due

to performance and resource considerations.

  * A file that was opened once remains within the persistent document
model.  This means the effect to recheck a theory hierarchy from the
point of that file happens only once, when it is first opened.  Later
it can be closed and re-opened without any change.

  * The main portion of semantic ML markup is now maintained persistently
in ML, and sent to the Scala side via some Execution.print function,
which is asynchronous, depends on perspective, and non-persistent.
This means, whenever some already processed ML file is visited in the
editor, substantial amounts of reports are sent over the wire on the
spot -- there is a deep purple flash seen on the ML_file command.
When the file becomes invisible later, these resources are freed 
after

some timeout and the JVM gets a chance to perform GC eventually.

With this increasingly complex setup --- scalability is never for free 
--- I can now process Main.thy with all ML files from 
src/HOL/Tools/BNF/ into the IDE. The JVM requires less than 1.5 GB and 
ML about 2 GB.


This is great, especially since BNF is now distributed all over 
HOL---some parts (Ctr_Sugar.thy) are loaded very early, some in the 
middle (up to BNF_LFP.thy), and some towards the end, even after 
List.thy (BNF_GFP.thy). Now I can lookup library functions loaded in 
Ctr_Sugar, when working on the ML files in BNF_GFP without waiting for 
everything in between to reload.


Do I understand the third bullet point correctly, in that closing ML 
buffers is not required anymore (to save space), since the memory 
associated to unfocused buffers will be freed by GC eventually?


Thanks for the hard work towards the best IDE for a functional 
programming language!

Dmitriy

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] set_comprehension_pointfree simproc

[Dmitriy Traytel]

Am 14.03.2014 13:36, schrieb Makarius:

What is the status of the set_comprehension_pointfree simproc?

In 31afce809794 Dmitriy says set_comprehension_pointfree simproc 
causes to many surprises if enabled by default, and in 4d899933a51a 
I've tried to reconstruct the missing NEWS entry, since this is cleary 
a user-relevant change.


Looking around in the sources and the history, e.g. 9979d64b8016 where 
Lukas Bulwahn is moving simproc from Finite_Set to more appropriate 
Product_Type theory shows that there is a related 
Set_Comprehension_Pointfree.code_simproc still present today 
http://isabelle.in.tum.de/repos/isabelle/annotate/9979d64b8016/src/HOL/Product_Type.thy#l1127


When working towards 31afce809794, I also tried deactivating this code 
preprocessor, but it was used in some places outside of HOL-Main for 
code generation (e.g. in HOL-IMP).


Does anybody understand how the tool was initially intended to work?  
Is it feasible to move it just in one place?  Lets say 
src/HOL/Library/Set_Comprehension_Pointfree.thy, so that the 
applications that need it can import just that theory, and main HOL 
remains clear.
Yes, that's a good idea. The is one usage of the simproc in HOL 
(Relation.thy), but this should be easy to get rid of.


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: improved support for Isabelle/ML

[Dmitriy Traytel]

Hi Makarius,

Am 17.02.2014 14:14, schrieb Makarius:
* Improved support for Isabelle/ML, with jEdit mode isabelle-ml for 
auxiliary ML files.


This refers to Isabelle/56ebc4d4d008.  It continues recent 
improvements of auxiliary file support.


The IDE support for Isabelle/ML is already quite substantial, but with 
every step forward, I get 5 new ideas what else could be done.  I am 
curious to hear what early-adopters and testers of the Isabelle 
repository say.
I've tried it out when working on what is now Isabelle/fd9ea8ae28f6. It 
is really great to see the error messages where they belong to and to 
have the type annotations everywhere now also in ML files (just as in 
embedded Isabelle/ML blocks). The new colors are also nice ;-).


However, once I had to restart Isabelle as JEdit became quite 
irresponsive (using almost 4GB of memory, forced GC didn't help). Maybe 
I just hat too many ML files open (I usually don't close them once 
opened) or my ML files are just too big: e.g. 
~~/src/HOL/Tools/BNF/bnf_gfp.ML, although on a fresh start after opening 
just this ML file the system is responsive (with some understandable 
delay in displaying the markup, but instantly processing edits). Maybe 
slightly lighter type annotations (at every constant/variable rather 
than at every subterm) would dodge such problems?


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL/Library/Code_Prolog.thy breakdown

[Dmitriy Traytel]

Am 13.02.2014 12:48, schrieb Makarius:

Today isatest has reported a breakdown of HOL/Library/Code_Prolog.thy.

This was undetected in a more regular test due to this change that 
removed it from the normal HOL-Library session:


changeset:   38504:76965c356d2a
user:haftmann
date:Wed Aug 18 09:46:59 2010 +0200
files:   src/HOL/Library/ROOT.ML 
src/HOL/Tools/Predicate_Compile/code_prolog.ML

description:
removed Code_Prolog: modifies global environment setup non-conservatively


The mysterious modification of the global environment above was a 
redefined outer syntax command values, with slightly different 
behaviour than the normal one.  Such a poke into the outer syntax 
affects the whole prover process, it escapes the context of the loaded 
theory and provokes erratic behaviour.


The ability to redefine outer syntax commands is merely an accidental 
left-over from the distant past.  It is required in interactive mode, 
to allow repeated processing of the (one!) command definition, but 
even that restricted scheme is apt to surprises as everybody knows.



So apart from some repairs of 
src/HOL/Tools/Predicate_Compile/code_prolog.ML in a76c679c0218, the 
changeset e42a3fc18458 makes more clear (in batch mode) that 
redefining outer syntax commands is not supposed to happen.  This 
provides a window of opportunity to remove spurious redefinitions 
elsewhere, until the coming release.
If nobody stops me, I will take care of 
~~/src/HOL/ex/Interpretations_with_Defs. It's redefinition of the 
interpretation command disturbed me already for a while.


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-IMP very slow

[Dmitriy Traytel]

Should be fine again (or at least better) with b445c39cc7e9. Thanks for 
the notification.


Dmitriy

Am 12.02.2014 16:28, schrieb Makarius:
Tests about slowness take long, but here is a presumably good point in 
the published history:


Isabelle/db691cc79289
Finished Pure (0:00:10 elapsed time, 0:00:12 cpu time, factor 1.20)
Finished HOL (0:02:13 elapsed time, 0:05:56 cpu time, factor 2.67)
Finished HOL-IMP (0:01:58 elapsed time, 0:07:28 cpu time, factor 3.79)

It probably corresponds to AFP/08874371d79e.

This might help someone to detach for a few hours or days, until the 
public history is back to normal and in a testable state.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] text_fold

[Dmitriy Traytel]

Am 10.02.2014 14:18, schrieb Makarius:

On Mon, 25 Nov 2013, Dmitriy Traytel wrote:


Am 23.11.2013 19:42, schrieb Makarius:

 On Mon, 28 Oct 2013, Dmitriy Traytel wrote:

  Concerning the error messages: at least you should always get   
strictly more information than without coercion inference (i.e. the 
  error message of the standard type-inference will always come 
first,   only then coercion inference will give additional hints). 
Of course,   the additional information can be distracting---maybe 
it should be   hidden in a popup or so).


 Concerning the popup or so you could experiment with
 Pretty.text_fold (although the fold will be always open by default in
 currently published Isabelle versions).

 The Isabelle Pretty module started out as implementation of
 Oppen-style pretty-printing by Larry Paulson, but it has acquired more
 and more logical markup facilities over the years (e.g. Pretty.markup,
 Pretty.paragraph, Pretty.item).

 The full potential of this is still unused.  (Display of advanced 
markup

 requires a proper PIDE front-end.)
Thanks for the hint. There result of my experiments are in the 
development repository (2bbcbf8cf47e).


This thread that originated from isabelle-users is still somehow open, 
see
also 
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-October/msg00183.html



In Isabelle/35354009ca25 I have sorted out some misunterstandings 
about Markup and Pretty.


Pretty.text_fold is fine if you assemble pretty trees, but having 
already formatted strings means you can't go through a pretty tree 
again: Pretty.str assumes an atomic argument.  (There used to be a 
mostly forgotten ML naming convention, to use str for unformatting 
strings and string for formatted ones, cf. Pretty.str vs. 
Pretty.str_of vs. Pretty.string_of.)

I see. Thanks for repairing this.



The reason why that API mismatch was not immediately detected is that 
Isabelle/Scala does its own rendering of pretty trees, from the 
overall output produced by the prover.  This occasionally hides 
Isabelle/ML programming mistakes concerning Pretty.T, until someone 
uses a historical Isabelle front-end, or does Isabelle latex pretty 
printing.



Using Markup.text_fold and already formatted strings in 35354009ca25 
makes the situation formally more correct, and simpler.  What I can't 
test here are all the individual error messages, because I don't know 
how to provoke them.  I've merely done a sanity check with the 
original example from 
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-October/msg00208.html


There are (commented) test cases for some of them in 
~~/src/HOL/ex/Coercion_Examples.thy . I've checked those now and they 
seem fine.


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] AFP failures

[Dmitriy Traytel]

Zorn is supposed to move to Main together with the new (co)datatype 
package. I guess it was removed from Library only by mistake.


Dmitriy

Am 26.11.2013 12:58, schrieb Lawrence Paulson:

Of course we don’t have any formal curation policy for the library, but Zorn's 
lemma is a fundamental result. Perhaps we need to think about what things are 
and are not allowed in the library. Deleting things will always be risky.

Larry

On 26 Nov 2013, at 11:30, Johannes Hölzl hoe...@in.tum.de wrote:


Looks like Zorn's lemma is not included in HOL-Library anymore. When
Coinductive loads Zorn it is also included in the Latex document. (Zorn
uses \sqsubset in a local)

I added now Zorn to HOL-Library (isa# acb41098607a), at least
Coinductive works now.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Outdated state after opening theories from images

[Dmitriy Traytel]

This refers to Isabelle/d71c2737ee21.

The minimal example is really minimal this time:

theory Scratch
imports Main
begin

end

In Isabelle/jEdit this loads fine. Then Control+click on Main, wait a 
moment for the text to turn #EEE3E3, close Main.thy and Scratch.thy is 
now outdated as well. The only thing that helps now is a jEdit restart.


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Outdated state after opening theories from images

[Dmitriy Traytel]

Am 22.11.2013 21:40, schrieb Makarius:

On Fri, 22 Nov 2013, Dmitriy Traytel wrote:


This refers to Isabelle/d71c2737ee21.

The minimal example is really minimal this time:

theory Scratch
imports Main
begin

end

In Isabelle/jEdit this loads fine. Then Control+click on Main, wait a 
moment for the text to turn #EEE3E3, close Main.thy and Scratch.thy 
is now outdated as well. The only thing that helps now is a jEdit 
restart.


That is a hard crash of the PIDE protocol handler in Isabelle/ML. It 
should now work better with 31844ca390ad.


This is a follow-up to the recently added support for auxiliary files 
(via 'ML_file' etc.) within the Prover IDE (05738b7d8191 and before).


Thanks for the patch and the very useful feature for people working with 
Isabelle/ML.


Dmitriy

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle2013-2 release

[Dmitriy Traytel]

From my angle Isabelle/f6ffe53387ef resolves [1] in a robust way. But 
I'm waiting for Christian to confirm this.


Dmitriy

Am 21.11.2013 00:13, schrieb René Neumann:

If there will already be a new release, would it perhaps be possible to
merge the fix (given there is a robust one) for this 'adhoc_overloading
raises TYPE' issue [1] ?

This error is quite puzzling. And it occurs even if one does not know
what the packages 'adhoc_overloading' and 'coercions' are about;
depending on theories using it (e.g. ICF) is sufficient.

This is just meant as a plain question. I fully understand that this
change might be seen as 'too large on this short notice'.

Thanks,
René

[1]
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-November/msg00146.html
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Sledgehammer proof text insertion

[Dmitriy Traytel]

Am 05.09.2013 13:35, schrieb Florian Haftmann:

I also observed that if you use sledgehammer as old-style keyword, the
proof text is inserted after instead of just replacing


lemma
   distinct xs ⟹ n ≠ m ⟹ n  length xs ⟹ m  length xs ⟹ xs ! n ≠ xs ! m
   sledgehammer by (metis distinct_conv_nth)

But maybe in the presence of the panel it is not worth worrying about this.

The same applies to try0 for which there is no panel (yet?).

Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] New (Co)datatypes: Status Plan (FYI)

[Dmitriy Traytel]

Am 04.08.2013 18:57, schrieb Florian Haftmann:

For nonnested recursive datatypes, compatibility is quasi-100%; and for nested
datatypes, the package will support an optional nested to mutual reduction to
simulate the old package, so that the same theorems as before are available
(albeit under different names).

has an explicit need for a »nested to mutual« mode ever been
articulated?  In my personal opinion this construction has always
appeared counter-intuitive, because the inherent redundancy with an
existing type springs to your eyes after you have done this game a few
times.  Maybe a chance to save some work.
I also find it always counter-intuitive when I have to use it (of course 
the have to will not apply anymore in our case). However the 
mutualized primrec seems to be more flexible. Without the 
mutualization, in order to define a primitive recursive function on say


datatype 'a tree = Node 'a 'a tree list

one is allowed to apply the recursive calls through the map on lists 
only. Defining a function that additionally filters the nested list of 
children becomes counter-intuitive then.


There is also a more technical reason why we want to perform the nested 
to mutual reduction: It gives us a very cheap compatibility layer for 
the old package. I.e. everything that is defined by the new package and 
falls into the fragment of the old package can be registered as an old 
datatype benefiting from all the infrastructure built around it (e.g. 
size function, Quickcheck, and other datatype interpretations). We 
expect this actually to save much work, compared to reimplementing that 
functionality now before moving to Main (instead we can do it in a lazy 
fashion).


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] lemma addition

[Dmitriy Traytel]

Am 25.07.2013 04:16, schrieb Christian Sternagel:

Dear developers,

While the following lemma is proved automatically

  lemma converse_subset:
  A¯ ⊆ B¯ ⟷ A ⊆ B by auto

I'm not sure exactly how, since simp_trace shows no application of 
simplification rules and neither of the rules suggested by different 
ATPs through sledgehammer are -- as far as I can tell -- automatic 
rules in the sense of [intro], [elim], [dest].


Sledgehammer indicates that the following lemmas are relevant in the 
proof:


always: converse_Un converse_converse
plus either of:
  - inf_absorb2 and inf_le1
  - subset_Un_eq
  - le_iff_inf

Anyway, I found this lemma useful to have around explicitly. Maybe it 
could be added to Relation.thy? Any thoughts?
I think the usual policy is to have at least two applications before 
adding such a lemma. However we use the corresponding lemma about 
conversep in the (co)datatype package. Since the latter will sooner or 
later become part of the HOL session anyway, I think it's fine to add 
both versions to Relation.thy. I'll do that (under the name 
converse(p)_mono).


Dmitriy

PS: for me this looks like an isabelle-users thread ;-)

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] type unification

[Dmitriy Traytel]

If you are planing to localize the thing, you'll have to take the 
context into account. I guess you don't want to generalize over fixed 
type variables (as your solution does).


locale A =
fixes a :: 'a
begin

ML {*
  val T1 = @{term a} | singleton (Variable.polymorphic @{context}) | 
fastype_of
  val T2 = @{term a} | (fastype_of # Term.map_type_tfree (TVar o 
apfst (rpair 0)))

*}

end

Dmitriy

Am 11.07.2013 09:01, schrieb Christian Sternagel:

Dear Dimitriy,

thanks that does the trick. However, after having a look at the 
implementation of Variable.polymorphic, I'm wondering whether it isn't 
overkill in my case. What about


  fastype_of # Term.map_type_tfrees (TVar o apfst (rpair 0))

as alternative?

Since I'm manually naming schematic type variables apart before 
unification anyway, shouldn't that also work (without ever using a ctxt)?


cheers

chris

On 07/11/2013 02:57 PM, Dmitriy Traytel wrote:

Hi Chris,

I think Variable.polymorphic is what you want to use before using
fastype_of.

Dmitriy

Am 11.07.2013 05:12, schrieb Christian Sternagel:

Dear list,

what is the proper way of obtaining a type from a term, in case I want
to give it as argument to Sign.typ_unify (of Sign.typ_match for that
matter)?

My question arises as follows. In adhoc_overloading.ML previously
Sign.the_const_type was used to obtain the type of a constant. The
result is a type with schematic type variables. Now that I want to use
terms instead of constants (as strings) I replaced Sign.the_const_type
by fastype_of, but this yields a type with fixed type variables and
thus unification may fail. So once again: What is the proper way of
getting a schematic type from a term?

cheers

chris

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 







___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] type unification

[Dmitriy Traytel]

Hi Chris,

I think Variable.polymorphic is what you want to use before using 
fastype_of.


Dmitriy

Am 11.07.2013 05:12, schrieb Christian Sternagel:

Dear list,

what is the proper way of obtaining a type from a term, in case I want 
to give it as argument to Sign.typ_unify (of Sign.typ_match for that 
matter)?


My question arises as follows. In adhoc_overloading.ML previously 
Sign.the_const_type was used to obtain the type of a constant. The 
result is a type with schematic type variables. Now that I want to use 
terms instead of constants (as strings) I replaced Sign.the_const_type 
by fastype_of, but this yields a type with fixed type variables and 
thus unification may fail. So once again: What is the proper way of 
getting a schematic type from a term?


cheers

chris

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Global build failures of the AFP in the testboard

[Dmitriy Traytel]

Am 15.05.2013 15:48, schrieb Makarius:
What is still unclear to me after so many years of testboard is how it 
actually used in practice.  I just do isabelle build -j4 -a -d 
'$AFP' to see immediately how everything works out.  It is also 
possible to make a quick integrity check via isabelle build -n -a -d 
'$AFP'.
Actually, isabelle build -j4 -a -d '$AFP' was almost exactly what I 
did before I ran into this error. Here, I've used the testboard merely 
as a reference.


Another use case is the process making SML/NJ happy. I am aware that it 
is currently (e.g. in 4517ceb545c1) unhappy about BNFs.


But there are also heavier users of the testboard than me.

Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Global build failures of the AFP in the testboard

[Dmitriy Traytel]

Am 15.05.2013 16:34, schrieb Makarius:

On Wed, 15 May 2013, Dmitriy Traytel wrote:


Am 15.05.2013 15:48, schrieb Makarius:
What is still unclear to me after so many years of testboard is how 
it actually used in practice. I just do isabelle build -j4 -a -d 
'$AFP' to see immediately how everything works out.  It is also 
possible to make a quick integrity check via isabelle build -n -a 
-d '$AFP'.
Actually, isabelle build -j4 -a -d '$AFP' was almost exactly what I 
did before I ran into this error. Here, I've used the testboard 
merely as a reference.


Another use case is the process making SML/NJ happy. I am aware that 
it is currently (e.g. in 4517ceb545c1) unhappy about BNFs.


I am using the mira results on http://isabelle.in.tum.de/reports/Isabelle
myself a lot to navigate quickly to points where Isabelle and AFP 
diverge.


Is that already testboard?  I thought that would be a slightly 
different mode of operation to check quasi-interactively if something 
is ready for push.
Right, I should have referenced reports rather than testboard. From 
that perspective I use the testboard even less.


Dmitriy

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Case translations as a separate check phase independent of the datatype package

[Dmitriy Traytel]

On 24.04.2013 16:18, Brian Huffman wrote:

On Wed, Apr 24, 2013 at 2:52 AM, Dmitriy Traytel tray...@in.tum.de wrote:

However, your example is still not printed as expected (assuming that the
output should be equal to the input in this case):

(case x of (a, b) = λ(c, d). e) y

Usually prod_case is printed as a tuple-lambda when partially
applied, and as a case expression when fully applied. So considering
that the underlying term in my example is prod_case (λa b. prod_case
(λc d. e)) x y, the above output makes perfect sense.
I see. Previously, I though that prod_case is always supposed to be 
printed as a lambda with a pattern and the fact that it is printed as a 
case expression sometimes is a coincidence caused by the order in which 
syntax translations are applied. But your explanation makes sense and 
results in less work for me :-)


Dmitriy

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Global build failures of the AFP in the testboard

[Dmitriy Traytel]

Hi all,

since Containers are in the AFP mira results in global crashes of the 
build tool 
(http://isabelle.in.tum.de/testboard/Isabelle/report/2cef0644d3d7416f8d7cea92e24fd694). 
By global I mean that no session is built at all due to an outdated (wrt 
Isabelle repository, e.g. 916271d52466) import of 
src/HOL/Library/Efficient_Nat.thy in the session Containers-Benchmarks.


For now I commented the Containers-Benchmarks session out (AFP/ 
99c45df7f5af) - now the test will reveal further outdated constructs in 
Containers (mostly related to Florian's reform of the code generation 
for numerals).


The question remains, whether it is possible for the build tool to 
proceed with other sessions if the imports of a single session are faulty.


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Case translations as a separate check phase independent of the datatype package

[Dmitriy Traytel]

Hi Brian

thanks for the report. Isabelle/cf039b3c42a7 resolves this in the sense 
that internal constants (like case_guard) are not visible anymore.


However, your example is still not printed as expected (assuming that 
the output should be equal to the input in this case):


(case x of (a, b) ⇒ λ(c, d). e) y

I think, the proper resolution to this is to have an uncheck phase for 
turning prod_case e intro λ(x, y). e x y before the case translation 
uncheck phase. Maybe Makarius or Stefan could comment on this. Then, I 
could have a look.


Dmitriy

On 24.04.2013 02:10, Brian Huffman wrote:

I discovered a problem with the pretty-printing of some terms (I am
using revision 4392eb046a97).

term (λ(a, b) (c, d). e) x y

case_guard True x
   (case_cons (case_abs (λa. case_abs (λb. case_elem (a, b) (λ(c, d). e
 case_nil)
   y
   :: 'e

I assume this is a result of the recent changes to the handling of
case expressions?

- Brian


On Wed, Apr 10, 2013 at 9:16 AM, Dmitriy Traytel tray...@in.tum.de wrote:

* Nested case expressions are now translated in a separate check
   phase rather than during parsing. The data for case combinators
   is separated from the datatype package. The declaration attribute
   case_tr can be used to register new case combinators:

   declare [[case_translation case_combinator constructor1 ... constructorN]]

This refers to Isabelle/bdaa1582dc8b

Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Case translations as a separate check phase independent of the datatype package

[Dmitriy Traytel]

Hi Brian,

this is indeed somehow complicated.

Almost everything in the new shallow syntax translation and in the new 
check phase destructs and constructs the function type. An example is 
the print translation case_tr' in ~/src/HOL/Tools/case_translation.ML 
which relies on Sign.add_advanced_trfuns to destruct the functional 
arguments to the syntactic constant case_guard.


I see two possible solutions:

1) Code duplication with appropriate handling of Rep_cfun and Abs_cfun 
(parameterizing everything with functions like strip_comb/dest_comb is 
not feasable IMO).
2) Shallow syntactic translation of constants over continuous functions 
into unspecified (syntactic) constants over functions, which is reverted 
in a check phase after being processed by the case translation phase. 
The attached theory shows how this could look like (the check phase is 
really ad-hoc there, one would need to know precisely what functions are 
supposed to be converted back to continuous functions).


However, both alternatives seem not to be very clean.

Dmitriy

On 16.04.2013 01:46, Brian Huffman wrote:

It would be nice to get HOLCF case combinators working with this new
system, as the parsing for HOLCF case expressions has been a bit
broken for some time.

Can case combinators and constructor functions with
continuous-function types be made to work with the case_tr (or
case_translation?) attribute? Even if we need a separate
HOLCF-specific attribute, might it be possible to get HOLCF case
expressions to work with the new translation check phase?

- Brian

On Wed, Apr 10, 2013 at 9:16 AM, Dmitriy Traytel tray...@in.tum.de wrote:

* Nested case expressions are now translated in a separate check
   phase rather than during parsing. The data for case combinators
   is separated from the datatype package. The declaration attribute
   case_tr can be used to register new case combinators:

   declare [[case_translation case_combinator constructor1 ... constructorN]]

This refers to Isabelle/bdaa1582dc8b

Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




Case_HOLCF.thy
Description: application/isabelle-theory
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Where are the error messages?

[Dmitriy Traytel]

Hi,

theory Scratch
imports Main
begin

term True x
thm TrueI[OF TrueI]

end

behaves very strangely in jedit with Isabelle/5dbe537087aa. For both 
commands there is no indication of errors (except of the absence of a 
popup). This seams to apply to all Isar commands involving 
Toplevel.no_timing.


Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Automated testing questions

[Dmitriy Traytel]

Hi Clemens,

On 17.03.2013 20:43, Clemens Ballarin wrote:

Dear Developers,

What it the current best practice for testing my change to Isabelle?  
There used to be testboard, but I'm unsure how that evolved.  Is there 
a similar service for testing my change to Isabelle against the AFP?
I do use the testboard for bigger changesets. The description from 
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg01500.html 
(Developer-initiated tests) is AFAIK still up to date.


Another alternative is to build everything on your own machine, which is 
feasible thanks to the wonders of PolyML 5.5 and the new build system. 
All you need to do is to clone the AFP repository, register it as a 
component (via init_component /path/to/AFP in etc/settings) and follow 
the instruction from 
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02903.html 
.


Also, which server should I use for pushing my changes to Isabelle so 
as to avoid repository trouble?

lxbroy10

Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Repository trouble

[Dmitriy Traytel]

I'm looking intro it.

Dmitriy

On 21.12.2012 04:07, Christian Sternagel wrote:

Dear all,

just now, when I tried

  hg in

in the development repo, I got the error below. My mercurial version 
is 2.2.3 (for at least some weeks). Did anybody else experience 
similar problems?


cheers

chris

comparing with http://isabelle.in.tum.de/repos/isabelle
searching for changes
changeset:   50600:48c0c3bc40dd
** unknown exception encountered, please report by visiting
**  http://mercurial.selenic.com/wiki/BugTracker
** Python 2.7.3 (default, Jul 24 2012, 10:05:38) [GCC 4.7.0 20120507 
(Red Hat 4.7.0-5)]

** Mercurial Distributed SCM (version 2.2.3)
** Extensions loaded: graphlog, mq, rebase, color, pager
Traceback (most recent call last):
  File /usr/bin/hg, line 38, in module
mercurial.dispatch.run()
  File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, 
line 27, in run

sys.exit((dispatch(request(sys.argv[1:])) or 0)  255)
  File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, 
line 64, in dispatch

return _runcatch(req)
  File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, 
line 87, in _runcatch

return _dispatch(req)
  File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, 
line 696, in _dispatch

cmdpats, cmdoptions)
  File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, 
line 472, in runcommand

ret = _runcommand(ui, options, cmd, d)
  File /usr/lib64/python2.7/site-packages/mercurial/extensions.py, 
line 184, in wrap

return wrapper(origfn, *args, **kwargs)
  File /usr/lib64/python2.7/site-packages/hgext/pager.py, line 91, 
in pagecmd

return orig(ui, options, cmd, cmdfunc)
  File /usr/lib64/python2.7/site-packages/mercurial/extensions.py, 
line 184, in wrap

return wrapper(origfn, *args, **kwargs)
  File /usr/lib64/python2.7/site-packages/hgext/color.py, line 362, 
in colorcmd

return orig(ui_, opts, cmd, cmdfunc)
  File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, 
line 786, in _runcommand

return checkargs()
  File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, 
line 757, in checkargs

return cmdfunc()
  File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, 
line 693, in lambda

d = lambda: util.checksignature(func)(ui, *args, **cmdoptions)
  File /usr/lib64/python2.7/site-packages/mercurial/util.py, line 
463, in check

return func(*args, **kwargs)
  File /usr/lib64/python2.7/site-packages/mercurial/extensions.py, 
line 139, in wrap

util.checksignature(origfn), *args, **kwargs)
  File /usr/lib64/python2.7/site-packages/mercurial/util.py, line 
463, in check

return func(*args, **kwargs)
  File /usr/lib64/python2.7/site-packages/hgext/mq.py, line 3396, in 
mqcommand

return orig(ui, repo, *args, **kwargs)
  File /usr/lib64/python2.7/site-packages/mercurial/util.py, line 
463, in check

return func(*args, **kwargs)
  File /usr/lib64/python2.7/site-packages/mercurial/extensions.py, 
line 139, in wrap

util.checksignature(origfn), *args, **kwargs)
  File /usr/lib64/python2.7/site-packages/mercurial/util.py, line 
463, in check

return func(*args, **kwargs)
  File /usr/lib64/python2.7/site-packages/hgext/graphlog.py, line 
560, in graph

return orig(*args, **kwargs)
  File /usr/lib64/python2.7/site-packages/mercurial/util.py, line 
463, in check

return func(*args, **kwargs)
  File /usr/lib64/python2.7/site-packages/mercurial/commands.py, 
line 3786, in incoming

return hg.incoming(ui, repo, source, opts)
  File /usr/lib64/python2.7/site-packages/mercurial/hg.py, line 501, 
in incoming

return _incoming(display, subreporecurse, ui, repo, source, opts)
  File /usr/lib64/python2.7/site-packages/mercurial/hg.py, line 470, 
in _incoming

displaychlist(other, chlist, displayer)
  File /usr/lib64/python2.7/site-packages/mercurial/hg.py, line 500, 
in display

displayer.show(other[n])
  File /usr/lib64/python2.7/site-packages/mercurial/cmdutil.py, line 
661, in show

self._show(ctx, copies, matchfn, props)
  File /usr/lib64/python2.7/site-packages/mercurial/cmdutil.py, line 
692, in _show

for tag in self.repo.nodetags(changenode):
  File /usr/lib64/python2.7/site-packages/mercurial/localrepo.py, 
line 468, in nodetags

if not self._tagscache.nodetagscache:
  File /usr/lib64/python2.7/site-packages/mercurial/util.py, line 
237, in __get__

result = self.func(obj)
  File /usr/lib64/python2.7/site-packages/mercurial/localrepo.py, 
line 395, in _tagscache

cache.tags, cache.tagtypes = self._findtags()
  File /usr/lib64/python2.7/site-packages/mercurial/localrepo.py, 
line 428, in _findtags

tagsmod.findglobaltags(self.ui, self, alltags, tagtypes)
  File /usr/lib64/python2.7/site-packages/mercurial/tags.py, line 
30, in findglobaltags

(heads, tagfnode, cachetags, shouldwrite) = _readtagcache(ui, repo)
  File /usr/lib64/python2.7/site-packages/mercurial/tags.py, line 
242, in _readtagcache

fnode = 

Re: [isabelle-dev] Repository trouble

[Dmitriy Traytel]

No one knows if somebody is doing something wrong.

I did a fresh clone (from the topmost non corrupted changeset) once 
again. Few commits are missing (I think by Jasmin and Sascha), as I 
didn't have them locally. You are both welcome to repush through 
lxbroy10 (please avoid macbroy20-29).


An empirical observation: hg verify mentioned Sledgehammer/MaSh again 
(just as when it exploded few days ago after my push).


Dmitriy

On 21.12.2012 08:16, Sascha Boehme wrote:

Hi,

It could have been caused by my commit last night. I am not sure what 
I did wrong, though.


Cheers,
Sascha

Von: Christian Sternagel
Gesendet: 21.12.2012 04:08
An: isabelle-dev
Betreff: [isabelle-dev] Repository trouble

Dear all,

just now, when I tried

   hg in

in the development repo, I got the error below. My mercurial version is
2.2.3 (for at least some weeks). Did anybody else experience similar
problems?

cheers

chris

comparing with http://isabelle.in.tum.de/repos/isabelle
searching for changes
changeset:   50600:48c0c3bc40dd
** unknown exception encountered, please report by visiting
**  http://mercurial.selenic.com/wiki/BugTracker
** Python 2.7.3 (default, Jul 24 2012, 10:05:38) [GCC 4.7.0 20120507
(Red Hat 4.7.0-5)]
** Mercurial Distributed SCM (version 2.2.3)
** Extensions loaded: graphlog, mq, rebase, color, pager
Traceback (most recent call last):
   File /usr/bin/hg, line 38, in module
 mercurial.dispatch.run()
   File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, line
27, in run
 sys.exit((dispatch(request(sys.argv[1:])) or 0)  255)
   File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, line
64, in dispatch
 return _runcatch(req)
   File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, line
87, in _runcatch
 return _dispatch(req)
   File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, line
696, in _dispatch
 cmdpats, cmdoptions)
   File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, line
472, in runcommand
 ret = _runcommand(ui, options, cmd, d)
   File /usr/lib64/python2.7/site-packages/mercurial/extensions.py,
line 184, in wrap
 return wrapper(origfn, *args, **kwargs)
   File /usr/lib64/python2.7/site-packages/hgext/pager.py, line 91, in
pagecmd
 return orig(ui, options, cmd, cmdfunc)
   File /usr/lib64/python2.7/site-packages/mercurial/extensions.py,
line 184, in wrap
 return wrapper(origfn, *args, **kwargs)
   File /usr/lib64/python2.7/site-packages/hgext/color.py, line 362,
in colorcmd
 return orig(ui_, opts, cmd, cmdfunc)
   File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, line
786, in _runcommand
 return checkargs()
   File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, line
757, in checkargs
 return cmdfunc()
   File /usr/lib64/python2.7/site-packages/mercurial/dispatch.py, line
693, in lambda
 d = lambda: util.checksignature(func)(ui, *args, **cmdoptions)
   File /usr/lib64/python2.7/site-packages/mercurial/util.py, line
463, in check
 return func(*args, **kwargs)
   File /usr/lib64/python2.7/site-packages/mercurial/extensions.py,
line 139, in wrap
 util.checksignature(origfn), *args, **kwargs)
   File /usr/lib64/python2.7/site-packages/mercurial/util.py, line
463, in check
 return func(*args, **kwargs)
   File /usr/lib64/python2.7/site-packages/hgext/mq.py, line 3396, in
mqcommand
 return orig(ui, repo, *args, **kwargs)
   File /usr/lib64/python2.7/site-packages/mercurial/util.py, line
463, in check
 return func(*args, **kwargs)
   File /usr/lib64/python2.7/site-packages/mercurial/extensions.py,
line 139, in wrap
 util.checksignature(origfn), *args, **kwargs)
   File /usr/lib64/python2.7/site-packages/mercurial/util.py, line
463, in check
 return func(*args, **kwargs)
   File /usr/lib64/python2.7/site-packages/hgext/graphlog.py, line
560, in graph
 return orig(*args, **kwargs)
   File /usr/lib64/python2.7/site-packages/mercurial/util.py, line
463, in check
 return func(*args, **kwargs)
   File /usr/lib64/python2.7/site-packages/mercurial/commands.py, line
3786, in incoming
 return hg.incoming(ui, repo, source, opts)
   File /usr/lib64/python2.7/site-packages/mercurial/hg.py, line 501,
in incoming
 return _incoming(display, subreporecurse, ui, repo, source, opts)
   File /usr/lib64/python2.7/site-packages/mercurial/hg.py, line 470,
in _incoming
 displaychlist(other, chlist, displayer)
   File /usr/lib64/python2.7/site-packages/mercurial/hg.py, line 500,
in display
 displayer.show(other[n])
   File /usr/lib64/python2.7/site-packages/mercurial/cmdutil.py, line
661, in show
 self._show(ctx, copies, matchfn, props)
   File /usr/lib64/python2.7/site-packages/mercurial/cmdutil.py, line
692, in _show
 for tag in self.repo.nodetags(changenode):
   File /usr/lib64/python2.7/site-packages/mercurial/localrepo.py,
line 468, in nodetags
 if not 

Re: [isabelle-dev] push request (Sublist.thy)

[Dmitriy Traytel]

On 17.12.2012 15:23, Makarius wrote:

On Thu, 13 Dec 2012, Dmitriy Traytel wrote:

I use Mercurial 2.2 and after pushing ed6b40d15d1c the attached error 
log was generated. hg verify on the server says that c4a27ab89c9b is 
the first damaged changeset. The corrupted repository is still on the 
server (/home/isabelle-repository/repos/isabelle.13.12.2012.backup).


We need to find more physical side-conditions for this kind of reactor 
meltdown.  What is your operating system platform?  Are you using 
bookmarks and/or patch queues locally?



Makarius
Ubuntu 12.10 (Linux kernel 3.5.0-20-generic, 64 bit). No bookmarks, but 
I do have a local patch queue. Also note that the changeset I was 
pushing (attached in previous mail on this thread), was imported via hg 
import (after adding the user name manually).


Dmitriy

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] push request (Sublist.thy)

[Dmitriy Traytel]

The test run was ok, but the repository is corrupted once again. Trying 
to repair by stripping.


Dmitriy

On 13.12.2012 13:23, Dmitriy Traytel wrote:
It worked for me. I'm currently building (or more precisely running 
the build tool ;-) ) and will push if it succeeds.


Dmitriy

On 13.12.2012 12:53, Tobias Nipkow wrote:
I tried to apply your patch but failed (see below). Since I had a 
problem with
somebody else's patch before, I wonder if something is wrong at my 
end? Any

suggestions?

Tobias

$ hg import emb
applying emb
patching file NEWS
Hunk #1 FAILED at 172
Hunk #2 FAILED at 181
2 out of 2 hunks FAILED -- saving rejects to file NEWS.rej
patching file src/HOL/BNF/Examples/TreeFI.thy
Hunk #1 FAILED at 11
1 out of 1 hunks FAILED -- saving rejects to file
src/HOL/BNF/Examples/TreeFI.thy.rej
patching file src/HOL/BNF/Examples/TreeFsetI.thy
Hunk #1 FAILED at 11
1 out of 1 hunks FAILED -- saving rejects to file
src/HOL/BNF/Examples/TreeFsetI.thy.rej
patching file src/HOL/Library/Sublist.thy
Hunk #1 FAILED at 2
Hunk #2 FAILED at 10
Hunk #3 FAILED at 22
Hunk #4 FAILED at 30
Hunk #5 FAILED at 42
Hunk #6 FAILED at 87
Hunk #7 FAILED at 105
Hunk #8 FAILED at 190
Hunk #9 FAILED at 206
Hunk #10 FAILED at 267
Hunk #11 FAILED at 419
11 out of 11 hunks FAILED -- saving rejects to file 
src/HOL/Library/Sublist.thy.rej

patching file src/HOL/Library/Sublist_Order.thy
Hunk #1 FAILED at 20
Hunk #2 FAILED at 39
2 out of 2 hunks FAILED -- saving rejects to file
src/HOL/Library/Sublist_Order.thy.rej
abort: patch failed to apply


Am 09/12/2012 12:50, schrieb Christian Sternagel:
I fixed an error that only came up during document preparation 
(which I should

have tested previously, sorry).

cheers

chris

On 12/09/2012 02:27 PM, Christian Sternagel wrote:

Dear all,

I have the following changes in my local patch queue:

- In src/HOL/Library/Sublist.thy:
renamed emb ~ list_hembeq and sub ~ sublisteq;
slightly changed definition of list_hembeq to make it reflexive
independent of the base order;
dropped predicate transp_on

Reasons: the name emb was very unspecific (hence the list_ 
prefix to

make clear that it is on lists, and h for homeomorphic since there
is an important difference between plain embedding (which is just 
the

sublist relation) and homeomorphic embedding, where we are allowed to
replace elements by smaller elements w.r.t. some base order) and in a
later development I will need an irreflexive variant (hence eq).
Furthermore, since the basic use of embedding is as a well-quasi-order
and wqos are reflexive it seems natural to have a definition where
embedding is reflexive independent of the base order.

I will add transp_on to Restricted_Predicates from the AFP. At some
point I would like to have the definitions of reflp_on, transp_on,
irreflp_on, antisymp_on, ... in the main distribution (but that is
an orthogonal issue).

Any comments? Any takers (for pushing my changes to the main repo)? I
checked the changes against f2241b8d0db5 with 'isabelle build -a' and
prepared a changeset for the AFP (which I can push myself).

cheers

chris

PS: As stated above, currently my changes are in my local patch queue
and I attached the corresponding patch file from .hg/patches (which
contains a commit message at the top). Should I transform this into an
hgbundle?


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 





This body part will be downloaded on demand.


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] push request (Sublist.thy)

[Dmitriy Traytel]

Stripping did not work (even on lxbroy10 with some older Mercurial). 
However, Johannes managed to apparently fix everything by doing a fresh 
clone, copying some files (such as hgrc) and adjusting permissions (cf. 
https://isabelle.in.tum.de/community/Reconstructing_the_Isabelle_repository).


Some more data points: I use Mercurial 2.2 and after pushing 
ed6b40d15d1c the attached error log was generated. hg verify on the 
server says that c4a27ab89c9b is the first damaged changeset. The 
corrupted repository is still on the server 
(/home/isabelle-repository/repos/isabelle.13.12.2012.backup).


Dmitriy

On 13.12.2012 13:58, Dmitriy Traytel wrote:
The test run was ok, but the repository is corrupted once again. 
Trying to repair by stripping.


Dmitriy

On 13.12.2012 13:23, Dmitriy Traytel wrote:
It worked for me. I'm currently building (or more precisely running 
the build tool ;-) ) and will push if it succeeds.


Dmitriy

On 13.12.2012 12:53, Tobias Nipkow wrote:
I tried to apply your patch but failed (see below). Since I had a 
problem with
somebody else's patch before, I wonder if something is wrong at my 
end? Any

suggestions?

Tobias

$ hg import emb
applying emb
patching file NEWS
Hunk #1 FAILED at 172
Hunk #2 FAILED at 181
2 out of 2 hunks FAILED -- saving rejects to file NEWS.rej
patching file src/HOL/BNF/Examples/TreeFI.thy
Hunk #1 FAILED at 11
1 out of 1 hunks FAILED -- saving rejects to file
src/HOL/BNF/Examples/TreeFI.thy.rej
patching file src/HOL/BNF/Examples/TreeFsetI.thy
Hunk #1 FAILED at 11
1 out of 1 hunks FAILED -- saving rejects to file
src/HOL/BNF/Examples/TreeFsetI.thy.rej
patching file src/HOL/Library/Sublist.thy
Hunk #1 FAILED at 2
Hunk #2 FAILED at 10
Hunk #3 FAILED at 22
Hunk #4 FAILED at 30
Hunk #5 FAILED at 42
Hunk #6 FAILED at 87
Hunk #7 FAILED at 105
Hunk #8 FAILED at 190
Hunk #9 FAILED at 206
Hunk #10 FAILED at 267
Hunk #11 FAILED at 419
11 out of 11 hunks FAILED -- saving rejects to file 
src/HOL/Library/Sublist.thy.rej

patching file src/HOL/Library/Sublist_Order.thy
Hunk #1 FAILED at 20
Hunk #2 FAILED at 39
2 out of 2 hunks FAILED -- saving rejects to file
src/HOL/Library/Sublist_Order.thy.rej
abort: patch failed to apply


Am 09/12/2012 12:50, schrieb Christian Sternagel:
I fixed an error that only came up during document preparation 
(which I should

have tested previously, sorry).

cheers

chris

On 12/09/2012 02:27 PM, Christian Sternagel wrote:

Dear all,

I have the following changes in my local patch queue:

- In src/HOL/Library/Sublist.thy:
renamed emb ~ list_hembeq and sub ~ sublisteq;
slightly changed definition of list_hembeq to make it reflexive
independent of the base order;
dropped predicate transp_on

Reasons: the name emb was very unspecific (hence the list_ 
prefix to
make clear that it is on lists, and h for homeomorphic since 
there
is an important difference between plain embedding (which is 
just the

sublist relation) and homeomorphic embedding, where we are allowed to
replace elements by smaller elements w.r.t. some base order) and in a
later development I will need an irreflexive variant (hence eq).
Furthermore, since the basic use of embedding is as a 
well-quasi-order

and wqos are reflexive it seems natural to have a definition where
embedding is reflexive independent of the base order.

I will add transp_on to Restricted_Predicates from the AFP. At some
point I would like to have the definitions of reflp_on, 
transp_on,
irreflp_on, antisymp_on, ... in the main distribution (but 
that is

an orthogonal issue).

Any comments? Any takers (for pushing my changes to the main repo)? I
checked the changes against f2241b8d0db5 with 'isabelle build -a' and
prepared a changeset for the AFP (which I can push myself).

cheers

chris

PS: As stated above, currently my changes are in my local patch queue
and I attached the corresponding patch file from .hg/patches (which
contains a commit message at the top). Should I transform this 
into an

hgbundle?


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 





This body part will be downloaded on demand.


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 



Übertrage nach 
ssh://macbroy21.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
Suche nach Änderungen
Entfernt: not trusting file /home/isabelle-repository/repos/isabelle/.hg/hgrc 
from untrusted user wenzelm, group isabelle
Entfernt

[isabelle-dev] set_comprehension_pointfree simproc losing bounds

[Dmitriy Traytel]

Hi all,

the following produces a Loose bound variable with Isabelle/4a15873c4ec9

theory Scratch
imports Main
begin

lemma finite {y |y. ∃x. y ∈ f x}
apply simp
oops

end

Fortunately, jedit treats a proof that used to work (but fails now due 
to the above) as a sorry, such that I can continue working on whatever 
follows in the theory until this issue is fixed.


Best wishes,
Dmitriy


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Dmitriy Traytel]

Hi all,

On 19.08.2011 01:38, Gerwin Klein wrote:
Should we ask a wider audience (isabelle-users) if anybody else has 
good reasons against/for a change?
Another small advantage of set as an own datatype arises in the context 
of subtyping.


We use map functions to lift coercions between base types to coercions 
between type constructors. E.g. nat list is subtype of int list with 
the coercion map int, provided that int is declared as a coercion 
and map as map function for 'a list. This is a typical example of a 
covariant map function (i.e. the lifting does not invert the direction 
of the subtype relation).


On the other hand, the generic map function for 'a = 'b (% f g h x. 
g (h (f x)) :: ('a = 'b) = ('c = 'd) = ('b = 'c) = ('a = 'd)) is 
contravariant in the first argument. Concretely that means that int = 
bool is a subtype of nat = bool, provided the above map function and 
the coercion int. In contrast, the corresponding map function for sets 
as predicates (image :: ('a = 'b) = ('a = bool) = ('b = bool)) 
is, as one would expect, covariant in the first argument.


The current implementation of subtyping allows to declare only one map 
function for a type constructor. Thus, we can have either the 
contravariant or the covariant map for the function type, but not both 
at the same time. The introduction of set as an own datatype would 
resolve this issue.


Cheers,
Dmitriy

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev