Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font
This is just to confirm that the result looks really great on my linux (Fedora 29 with i3) setup. Thanks! chris On 2/10/19 7:47 PM, Makarius wrote: > On 08/02/2019 10:03, Christian Sternagel wrote: >> >> I am glad to hear that others have the same experience, I thought my >> eyes were going bad ;) >> >> But seriously, "buy a new screen" is not always possible. For example, >> in the upcoming summer term I am teaching an Isabelle class at the >> University of Innsbruck. In my experience (and I just reconfirmed this >> for the room I will be teaching in), the projectors we have here a >> typically rather old (and have low resolution, but that is a different >> story). >> >> At the moment there is a palpable difference (font rendering crispness >> wise) between using Isabelle2018 with projector (which I will do anyway >> for my class) and some recent development version (sorry I didn't note >> down what changeset I used for testing my setup). > > Classic JDK 8 from Oracle and OpenJDK 11 (e.g. from AdoptOpenJDK) are > different in many ways, and it is definitely required to get used to the > new look of font rendering. (For me Isabelle2018 already looks very > strange.) > > With proper parameters -- in software and hardware -- fonts should come > out better than before. > > > First of all, sub-pixel rendering should be enabled, see this NEWS entry > from Isabelle/f714114b0571 (25-Oct-2018): > > *** Isabelle/jEdit Prover IDE *** > > * Improved sub-pixel font rendering (especially on Linux), thanks to > OpenJDK 11. > > (In Java 8, sub-pixel rendering made things worse.) > > Since that that NEWS entry is a bit too implicit, I have now changed the > default to enable "Subpixel HRGB" always on all platforms > (Isabelle/f610115ca3d0). I have checked my usual test machines for > Windows and macOS, to see that it all looks fine. > > > Secondly, I have done some more research on FreeType, the renderer used > for OpenJDK on Linux. It appears that the DejaVu family gets some > special treatment if it shows up under its original name, but not if it > is a renamed copy. So I have fine-tuned the Isabelle DejaVu fonts in > Isabelle/4791988fcbc4 to impose the FreeType auto-hinting beforehand to > the TrueType file: this leads to isabelle_fonts-20190210 in > Isabelle/7e5a7a11d5d1. > > > In summary: > > * Isabelle font rendering should be once again slightly better on Linux. > > * There is a small risk that it has slightly degraded on Windows and > macOS. > > In other words: early adopters should look closely if it is all fine. We > are (very slowly) moving towards the Isabelle2019 release (presumably > June 2019), and everything needs to be beyond doubt when released. > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font
Dear all, I am glad to hear that others have the same experience, I thought my eyes were going bad ;) But seriously, "buy a new screen" is not always possible. For example, in the upcoming summer term I am teaching an Isabelle class at the University of Innsbruck. In my experience (and I just reconfirmed this for the room I will be teaching in), the projectors we have here a typically rather old (and have low resolution, but that is a different story). At the moment there is a palpable difference (font rendering crispness wise) between using Isabelle2018 with projector (which I will do anyway for my class) and some recent development version (sorry I didn't note down what changeset I used for testing my setup). cheers chris On 2/5/19 11:43 AM, Peter Lammich wrote: > Hi list, > > I just updated my Isabelle devel version (now on d21789843f01), and > immediately noticed that the displayed fonts are significantly blurry. > > Find attached a side-by-side comparison of Isabelle-d21789843f01 (left) > and Isabelle-2018 (right). At least on my monitor, the font display on > the left side is significantly worse (blurred). Both use font size 18 > with standard anti-aliasing method. > > > Is this worsening due to another Java version, due to the new Isabelle > font, or has it some other reasons? How to find out? How to fix it? > > > -- > Peter > > > ___ > 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] AFP/HLDE
On 10/08/2018 04:14 PM, Makarius wrote: > On 08/10/18 15:58, Lars Hupel wrote: > > I don't mind if it is possible to eliminate AFP/HLDE (theory > Diophantine_Eqns_Lin_Hom.Solver_Code) outright, and just refrain from > doing such things in AFP. > Compiling a binary in HLDE was a mere experiment on our side too. So I also do not mind much to remove this again from the AFP. I would however like to keep theory Solver_Code and still let it generate Haskell source code (that is required for the handwritten Main.hs). Then the task of setting up a proper Haskell environment and compiling an executable is moved to prospective users. Which is fine with me. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP/HLDE
On 10/05/2018 10:14 PM, Makarius wrote: > > So the question is reduced by one step: What is the purpose of theory > "Solver_Code" abstractly? I just wanted to confirm that the purpose of Solve_Code is to produce a Haskell executable (that implements an algorithm that was formalized in the AFP entry). Or as you put it yourself: The abstract application I see here is: use Isabelle to produce some executable in Haskell (or OCaml, or Scala, or SML). cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP/HLDE
Dear Makarius On 10/05/2018 07:10 PM, Makarius wrote: > What is the purpose of the session HLDE, with its duplicate theory > Solver_Code that is also in Diophantine_Eqns_Lin_Hom? As the author of the corresponding ROOT file, when I look at it now, I cannot think of any reason to have also session HLDE (except of course the shorter name). cheers chris > > I've had seen odd crashes due to its non-temporary output into > ISABELLE_TMP, but the technical problem behind it might be actually in > Isabelle/Scala (rm_tree): > > Exception in thread "process_manager" java.nio.file.NoSuchFileException: > /tmp/isabelle-mawenzel/process7653301744367976304/HLDE/Main.hi > at > sun.nio.fs.UnixException.translateToIOException(UnixException.java:86) > > (Isabelle/742c88258cf8 + AFP/854bc290d72b + a derivative of "isabelle > dump" that is not in these repositories). > > > The HLDE session also touches the open question how to deal with > generated material in AFP. We have already a concept for "exports" in > Isabelle2018 (see NEWS). Maybe that is already sufficient that we can > make such sessions pure in the sense that nothing is written into odd > places in the file-system, only into the formal session database. > > > 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] NEWS: Isabelle server
Just for the record: Makarius' reply resolved the issue for me (see also below). On 05/09/2018 11:57 PM, Makarius wrote: > On 26/03/18 13:48, Christian Sternagel wrote: >> >> Thanks, I forgot about that option. >> >> With "isabelle latex" in the specified directory the error boils down to: >> >> ./root.tex:31: Package pdftex.def Error: File >> `isabelle-eps-converted-to.pdf' n >> ot found. >> >> See the pdftex.def package documentation for explanation. >> Type H for immediate help. >> ... >> >> Should isabelle-eps-converted-to.pdf exist on my system? > > I guess that the "epstopdf" tool is missing: there should be some Fedora > package for it. That is correct. Thanks for pointing it out, it was not clear to me from the error message. > > Anyway, in Isabelle/2a5ae592eafb the latex errors are again spilled into > user output -- this is required for hard errors of missing executables > and style files. > > With that I have managed to do "isabelle build -o document=pdf -g doc" > or "isabelle build_doc -a" sucessfully on Fedora 28: after cumbersome > saturation of the texlive installation, where almost every style file > has its own package. This kind of saturation is indeed cumbersome, but at least its possible as long as you know which packages are missing ;) cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle server
Dear Makarius, Thanks, I forgot about that option. With "isabelle latex" in the specified directory the error boils down to: ./root.tex:31: Package pdftex.def Error: File `isabelle-eps-converted-to.pdf' n ot found. See the pdftex.def package documentation for explanation. Type H for immediate help. ... Should isabelle-eps-converted-to.pdf exist on my system? cheers chris On 03/26/2018 01:26 PM, Makarius wrote: > On 26/03/18 09:33, Christian Sternagel wrote: >> >> I don't see a significant difference in output between my original >> >> isabelle build_doc system > >> *** Failed to build document in >> "/tmp/isabelle-griff/document_output1585848392449927242/system" >> >> and the suggested >> >> isabelle build -c -b System -o document=pdf -o document_output=output >> >> *** Failed to build document in >> "/home/griff/repos/tools/isabelle/src/Doc/System/output/system" >> >> I am still unclear on why "isabelle document" fails in both cases. > > The difference is the output directory. In the latter situation, you can > go there and inspect root.log or run pdflatex root manually. > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle server
Dear Makarius, I don't see a significant difference in output between my original isabelle build_doc system where I get ... isabelle document -d /tmp/isabelle-griff/document_output1585848392449927242/system -o pdf -n system *** Failed to build document in "/tmp/isabelle-griff/document_output1585848392449927242/system" and the suggested isabelle build -c -b System -o document=pdf -o document_output=output where I get ... isabelle document -d output/system -o pdf -n system *** Failed to build document in "/home/griff/repos/tools/isabelle/src/Doc/System/output/system" I am still unclear on why "isabelle document" fails in both cases. cheers chris PS: Anyway, I can get the manual from the URL you provided. Thanks! On 03/23/2018 11:51 AM, Makarius wrote: > On 23/03/18 10:29, Christian Sternagel wrote: >> >> Is there a way to get a more detailed report on why the last step, >> "isabelle document ...", failed? >> >> Btw: I also get (sometimes more specific) errors for building other >> documentation. >> >> Okay, turns out that I was missing the LaTeX packages >> >> nomencl, regexpatch, subfigure, supertabular >> >> on my system (Fedora 27). After installing those I still get some errors >> (all with similar error message): > > You can build all docs with detailed results like this: > > isabelle build -c -g doc -o document=pdf -o document_output=output > > > For the purpose of the updated system manual, you can now download the > nightly snapshot: https://isabelle.sketis.net/devel/release_snapshot > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle server
Dear Makarius, I am on 67927:0b70405b3969 and ./bin/isabelle build_doc system doesn't work for me. I get the error: Build started for documentation "system" Cleaning System ... Running System ... System FAILED ... isabelle document -d /tmp/isabelle-griff/document_output14698640433302927/system -o pdf -n system *** Failed to build document in "/tmp/isabelle-griff/document_output14698640433302927/system" Unfinished session(s): System Is there a way to get a more detailed report on why the last step, "isabelle document ...", failed? Btw: I also get (sometimes more specific) errors for building other documentation. Okay, turns out that I was missing the LaTeX packages nomencl, regexpatch, subfigure, supertabular on my system (Fedora 27). After installing those I still get some errors (all with similar error message): Running Tutorial ... Tutorial FAILED ... isabelle document -d /tmp/isabelle-griff/document_output1759007754075439311/tutorial -o pdf -n tutorial *** Failed to build document in "/tmp/isabelle-griff/document_output1759007754075439311/tutorial" Isar_Ref FAILED ... Codegen FAILED ... Prog_Prove FAILED ... Implementation FAILED ... Classes FAILED ... Eisbach FAILED ... Intro FAILED ... JEdit FAILED ... Logics FAILED ... Logics_ZF FAILED ... Nitpick FAILED ... Sledgehammer FAILED ... System FAILED ... Typeclass_Hierarchy FAILED cheers chris On 03/22/2018 05:30 PM, Makarius wrote: > On 19/03/18 19:35, Makarius wrote: >> *** System *** >> >> * The command-line tools "isabelle server" and "isabelle client" provide >> access to the Isabelle Server: it supports responsive session management >> and concurrent use of theories, based on Isabelle/PIDE infrastructure. >> See also the "system" manual. >> >> >> This refers to Isabelle/465f43a9f780. The chapter in the "system" manual >> provides general explanations, but lacks the description of specific >> server commands: these may be derived from >> src/Pure/Tools/server_commands.scala right now. > > I have made further refinements in Isabelle/0b70405b3969. The chapter in > the "system" manual now has almost 20 pages of explanations, including > various examples, see > http://isabelle.in.tum.de/repos/isabelle/file/0b70405b3969/src/Doc/System/Server.thy > or better its LaTeX rendering (e.g. via "isabelle build_doc system && > isabelle doc system"). > > The server should already be usable, but the following fine points are > still missing: > > * command "purge_theories" to get rid of results from "use_theories" > > * command "session_status" to provide continuous node_status > information, similar to the Theories dockable in Isabelle/jEdit > > >> It is only the start of a serious server, many more ideas are still in >> the pipeline, e.g. forwarding over an SSH tunnel that may >> disconnect/reconnect spontaneously. > > The SSH tunnel will require more work. It practically needs a way to > send theory files from the client OS context to the server OS context. > (All tools for that are there in Isabelle/Scala, but need to be fit > together in the proper way.) > > > 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
[isabelle-dev] some results about "lex"
Dear list, maybe the following results about "lex" are worthwhile to add to the library? lemma lex_append_right: "(xs, ys) ∈ lex r ⟹ length vs = length us ⟹ (xs @ us, ys @ vs) ∈ lex r" by (force simp: lex_def lexn_conv) lemma lex_append_left: "(ys, zs) ∈ lex r ⟹ (xs @ ys, xs @ zs) ∈ lex r" by (induct xs) auto lemma lex_take_index: assumes "(xs, ys) ∈ lex r" obtains i where "i < length xs" and "i < length ys" and "take i xs = take i ys" and "(xs ! i, ys ! i) ∈ r" proof - obtain n us x xs' y ys' where "(xs, ys) ∈ lexn r n" and "length xs = n" and "length ys = n" and "xs = us @ x # xs'" and "ys = us @ y # ys'" and "(x, y) ∈ r" using assms by (fastforce simp: lex_def lexn_conv) then show ?thesis by (intro that [of "length us"]) auto qed cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
Dear all, speaking of "chain", for me the main motivation of introducing "linked P" was in order to work well together with the corresponding generalizations of "take_while" and "drop_while", which are called "take_chain" and "drop_chain" in the AFP entry Efficient-Mergesort. E.g., "take_chain (op >) [3,2,1,2] = [3,2,1]" So besides very basic lemmas about "linked" (concerning append) there are some concerning its interaction with "take_chain" and "drop_chain" in Efficient_Sort.thy chris PS: another alternative name: "sorted_by" (I think the suffix "_by" is far more common -- e.g., in Haskekll -- than "_wrt"). On 08/16/2017 11:53 AM, Blanchette, J.C. wrote: > Hi Christian, Tobias, > >> I think your "sorted_wrt" is almost (modulo "fun" vs. "inductive") my >> "linked" from the AFP (Efficient_Mergesort). >> >> >> https://www.isa-afp.org/browser_info/current/AFP/Efficient-Mergesort/Efficient_Sort.html >> >> Maybe we could unify the constants/names somehow? >> >> At the moment I somewhat prefer "linked" (or maybe "linked_by") since >> sortedness implies that "P" is some kind of order, which it doesn't have >> to be. > > It also reminds me of my "derivation" predicate, which arose when formalizing > Bachmair & Ganzinger's chapter in the Handbook of Automated Reasoning: > > https://bitbucket.org/isafol/isafol/src/f0f585fb6cbd7097567cc1c493fe1b3c1223a8da/Bachmair_Ganzinger/Proving_Process.thy?at=master=file-view-default > > It's a bit different because of the use of lazy lists (to allow infinite > derivations) and the different handling of the empty list. > > Underlying all of these appears to be the concept of a "chain". That's what > we often call things of the form x1 > x2 > ... > xn (finite) or x1 > x2 > ... > (infinite), where > is some binary relation. In the context of Bachmair & > Ganzinger, or, indeed, for formalzing Definition 7.2.3 from Baader & Nipkow, > it makes sense to use a relation > that is not transitive. > > So maybe "chain" could be a good name for the finite concept? > > Incidentally, Georges Gonthier believes that for nonempty paths in a graph > (or more generally chains), the first element should be stored separately > from the other ones. I guess the main benefit is when concatenating two > paths, he can simply append. I'm not sure how relevant it is to us, though. > > 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] NEWS: Isabelle/VSCode
On 07/02/2017 10:59 PM, Makarius wrote: > On 02/07/17 22:16, Christian Sternagel wrote: >> >>> It should work analogously to the "Preview" button, but without having a >>> button. >> >> Preview (more concretely the "Open Preview" "button" -- some kind of >> magnifying glass icon where the rest is to tiny to discern) only gives >> me a white box with a very light gray copy of the theory file content. > > Odd. Is this really Isabelle_01-Jul-2017 as described in README.md -- or > alternatively current Isabelle/453f9cabddb5 ? The isabelle.home settings > of VSCode needs to point to the currect ISABELLE_HOME directory. Oh, I overlooked this part. I was still on ded1c636aece (the first version where I started looking into Isabelle/VSCode and did no longer remember README.md; but there where no error messages). Now I am on 453f9cabddb5. Sorry for that. > > You've also said that your VSCode is from the OS package repository. > Maybe it is better to use the official > https://code.visualstudio.com/Download I also updated VSCode (through its own interface) to the latest version from the above link. Now it works like you suggested. chris > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/VSCode
On 07/02/2017 02:21 PM, Makarius wrote: > On 02/07/17 13:31, Christian Sternagel wrote: >> On 07/01/2017 09:21 PM, Makarius Wenzel wrote: >>> There is also a "State" panel that imitates the dockable of the same >>> name in Isabelle/jEdit. You will get to that via the "isabelle.state" >>> command, e.g. use the SHIFT-CONTROL-P command palette and search for >>> "Isabelle" commands. It has the description "Show State". >> >> Nothing happens when I select (by clicking) "Isabelle: Show State" after >> SHIFT-CONTROL-P and searching for "Isabelle". > > You need to have an active theory file (with running prover process). I think I do (at least in "View ~> Output" I see subgoals when moving through a proof). > > It should work analogously to the "Preview" button, but without having a > button. Preview (more concretely the "Open Preview" "button" -- some kind of magnifying glass icon where the rest is to tiny to discern) only gives me a white box with a very light gray copy of the theory file content. chris > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/VSCode
On 07/01/2017 09:21 PM, Makarius Wenzel wrote: > On 01.07.17 20:46, Christian Sternagel wrote: >> >> It only took me some time to find the OUTPUT "panel" (View ~> Output) ;) > > That is a plain-text channel of VSCode. Oh, okay. > > There is also a "State" panel that imitates the dockable of the same > name in Isabelle/jEdit. You will get to that via the "isabelle.state" > command, e.g. use the SHIFT-CONTROL-P command palette and search for > "Isabelle" commands. It has the description "Show State". Nothing happens when I select (by clicking) "Isabelle: Show State" after SHIFT-CONTROL-P and searching for "Isabelle". chris > > Wiring up that GUI panel required a whole lot of tricks, but it should > be now trivial to make more panels. Although, this poses the problem of > multi-window management. > > > Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] unable to start Isabelle/jEdit due to error in unused session
Thanks Lars! I did not yet try your suggestion (and I am somewhat reluctant to install "3rd party" software for something I would consider basic functionality; but anyway, it's good to know that there is an alternative). Thanks Makarius! I even read the email you are referring to, but apparently this was too long ago ;) Anyway, what you suggest does in principle work (and shows that all the required functionality is already there). With isabelle jedit -R -l HOL I end up in Isabelle/HOL's ROOT file and everything after Pure has to be loaded. I am curious, is there a reason why it would not be a good idea to restrict to Session by default whenever isabelle jedit -l Sessions is invoked? Alternatively, something similar to "-R" but where I do not end up in a ROOT file and the specified session is already built (but none of its descendants is checked) might be convenient. cheers chris On 05/18/2017 10:34 AM, Makarius wrote: > On 18/05/17 09:03, Christian Sternagel wrote: >> >> I was just about to have a look at the latest and greatest Isabelle ( >> f35abc25d7b1 ) when I noticed the following behavior. >> >> I started with >> >> isabelle jedit -bf >> >> and then tried >> >> isabelle jedit -l HOL >> >> but got an error message about missing files (see PS for details). >> >> Now, these missing files are only referenced in IsaFoR's ROOT file (and >> the reason for the error is that IsaFoR is still running on >> Isabelle2006-1), which is read since IsaFoR is registered as an Isabelle >> component in my "etc/settings" > > See > http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg07321.html > > Quote: > > In current Isabelle/6acb28e5ba41 it is also possible to use something > like "isabelle jedit -R -l MY_SESSION" to restrict the theory name space > to the requirements of MY_SESSION. > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] unable to start Isabelle/jEdit due to error in unused session
Dear list, I was just about to have a look at the latest and greatest Isabelle ( f35abc25d7b1 ) when I noticed the following behavior. I started with isabelle jedit -bf and then tried isabelle jedit -l HOL but got an error message about missing files (see PS for details). Now, these missing files are only referenced in IsaFoR's ROOT file (and the reason for the error is that IsaFoR is still running on Isabelle2006-1), which is read since IsaFoR is registered as an Isabelle component in my "etc/settings" I think it would be convenient if 1) sessions that are not ancestors of "-l Session" are not checked on startup (or at least there was a way to activate this behavior), 2) or there was some easy way (e.g., a flag) to exclude specific Isabelle components / sessions / ROOT files from checks (without having to edit "etc/settings"). What do you think? cheers chris PS: The exact error message was /home/griff/repos/tools/isabelle/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar: Cannot start: *** No such file: "/home/griff/repos/tools/isabelle/src/HOL/Library/Fraction_Field.thy" *** The error(s) above occurred for theory "HOL-Lib.Fraction_Field" (line 17 of "/home/griff/repos/isafor/thys/ROOT") *** No such file: "/home/griff/repos/tools/isabelle/src/HOL/Library/Fundamental_Theorem_Algebra.thy" *** The error(s) above occurred for theory "HOL-Lib.Fundamental_Theorem_Algebra" (line 18 of "/home/griff/repos/isafor/thys/ROOT") *** No such file: "/home/griff/repos/tools/isabelle/src/HOL/Library/Polynomial_Factorial.thy" *** The error(s) above occurred for theory "HOL-Lib.Polynomial_Factorial" (line 29 of "/home/griff/repos/isafor/thys/ROOT") *** The error(s) above occurred in session "HOL-Lib" (line 1 of "/home/griff/repos/isafor/thys/ROOT") ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] code abbreviation for mapping over a fixed range
This email refers to the following commit: http://isabelle.in.tum.de/repos/isabelle/rev/7d1127ac2251 code abbreviation for mapping over a fixed range Is there a specific reason for this code equation: "map_range f (Suc n) = map_range f n @ [f n]" It seems rather inefficient. Anyway, what's the purpose of "map_range". cheers chris PS: I was confused about [code_abbrev], thus looked it up in isar-ref, then was further confused :D "code_abbrev" declares (or with option “del” removes) equations which are applied as rewrite rules to any result of an evaluation and symmetrically during preprocessing to any code equation or evaluation input. In my opinion the usage of the word "symmetrically" could be clarified. Does it mean "similar to the previous use case" or "symmetric in the sense of reading the equation from right to left"? signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] AFP devel not reachable
Dear all, http://afp.sourceforge.net/ seems to be down. Just out of curiosity: Does anyone know for how long and why? -cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: limited name space accesses
On 04/17/2015 12:04 AM, Makarius wrote: On Tue, 7 Apr 2015, Christian Sternagel wrote: PS: I'm still waiting for isabelle build -n -a -d '$AFP' -k qualified to finish (but I guess proper checking, taking semantics into account, is just expensive). Oops, while writing this email I obtained: *** java.lang.OutOfMemoryError: Java heap space 0:03:32 elapsed time, 0:05:46 cpu time, factor 1.63 (Maybe because in parallel I am still waiting on isabelle build -v -n -a -d '$AFP' -k hidden -k private ? Which seems to hangs at Session Pure/RAW now for several minutes.) Maybe this is just the normal behaviour of the JVM under low-memory conditions. I routinely have local settings like this: ISABELLE_BUILD_JAVA_OPTIONS=-Xms1024m -Xmx4096m -Xss4m Thanks for the hint! This even worked with two checks running in parallel (each of which finished in less than 4 minutes). cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: limited name space accesses
Very nice! I'll wait until the naming issue is settled before replacing my many uses of hide_const (open) A further naming suggestion: (a) private/hidden (b) qualified the latter is akin to Haskell's qualified import. cheers chris PS: I'm still waiting for isabelle build -n -a -d '$AFP' -k qualified to finish (but I guess proper checking, taking semantics into account, is just expensive). Oops, while writing this email I obtained: *** java.lang.OutOfMemoryError: Java heap space 0:03:32 elapsed time, 0:05:46 cpu time, factor 1.63 (Maybe because in parallel I am still waiting on isabelle build -v -n -a -d '$AFP' -k hidden -k private ? Which seems to hangs at Session Pure/RAW now for several minutes.) On 04/07/2015 02:07 PM, Makarius wrote: * Local theory specification commands may have a 'private' or 'restricted' modifier to limit name space accesses to the local scope, as provided by some context begin ... end block. For example: context begin private definition ... private definition ... private lemma ... lemma ... lemma ... theorem ... end This refers to Isabelle/83071f4c8ae6. After more than 10 years in the pipeline, and never-ending efforts to localize almost all tools, there is now the long anticipated limitation of name space accesses. There are presently two example applications: (1) Local tool setup with some auxiliary constants: induct_forall etc. in http://isabelle.in.tum.de/repos/isabelle/file/83071f4c8ae6/src/HOL/HOL.thy#l1377 (2) Plain specifications that are meant to produce theory-qualified names: AList.update etc. in http://isabelle.in.tum.de/repos/isabelle/file/e83ecf0a0ee1/src/HOL/Library/AList.thy#l11 I am still not 100% sure about the choice of keywords. There are two concepts that are supported: (a) totally inaccessible name space entry, (b) name space entry that is only accessible by qualified names, not the base name. Presently we have: (a) 'private' (b) 'restricted' I first started out implementing 'private' for the sake of Eisbach, which really needs that. Then I noticed that in practice one mostly uses 'restricted' to eliminated old hide (open), but this keyword is a bit awkward. Here are some possible alternatives: (a) 'hidden'(like Long_Name.hidden according to Isabelle/ML terminology) (b) 'private' (like 'private' in Java/Scala, in non-serious mode) or: (a) 'private' (like 'private' on Java/Scala in serious mode) (b) 'local' (like an ancient Isabelle command of that name) By non-serious mode I mean the rather easy way to bypass 'private' declarations on the JVM via reflection. Likewise our logical environment always allows to access inaccessible names, after some tweaking of the name space, e.g. via aliases. This could justify the use of 'private' for what is now 'restricted', or it might be just too confusing to users. Note that it is now releatively easy to test feasibility of new keywords like this: $ isabelle build -n -a -d '$AFP' -k hidden -k local 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] Isabelle gets stuck when imported theory is not found
Just for the record. I think I experienced something similar: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-January/005864.html cheers chris On 03/05/2015 11:39 AM, Johannes Hölzl wrote: In rev 304ee0a475d1 I fixed a problem that only appears when one loads ~~/src/HOL/Probability interactively based on the HOL image. In Measure_Space the theory Multivariate_Analysis was imported without the correct path. When started with -l HOL-Multivariate_Analysis it worked. Unfortunately there is no error message, it just looks like Isabelle/jEdit gets stuck at this point. Is there a way to show an error message at the position of the import header? - Johannes ___ 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] adhoc overloading: ugly output
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
# HG changeset patch
# Parent 4427f04fca57ea90f7fd8dbc271ac29a9268ec75
adhoc overloading must follow the same conventions as abbreviations
diff -r 4427f04fca57 -r fbefd978e72d src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.MLSun Jan 25 22:11:06 2015 +0100
+++ b/src/Tools/adhoc_overloading.MLTue Jan 27 13:59:16 2015 +0100
@@ -179,7 +179,9 @@
map (fn t = Term.map_aterms (insert_variants ctxt t) t);
fun uncheck ctxt ts =
- if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of)
ts then ts
+ if Proof_Context.abbrev_mode ctxt orelse
+Config.get ctxt show_variants orelse
+exists (can Term.type_of) ts then ts
else map (insert_overloaded ctxt) ts;
fun reject_unresolved ctxt =
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] TYPE_MATCH exception with adhoc_overloading
During a visit of Florian in Innsbruck we had some discussion on adhoc
overloading. One suspicion was that schematic type variables from
variants had to be paramified before using the resulting type unifier.
I tried to do so in the attached patch. Unfortunately, I still obtain
the following error in
~~/src/HOL/ex/Adhoc_Overloading_Examples.thy
Illegal schematic type variable: ?'a2
Please let me know if you have any comments on this topic (especially on
what is going on in the function unify_filter).
cheers
chris
On 01/20/2015 06:16 PM, Makarius wrote:
On Mon, 19 Jan 2015, Jasmin Blanchette wrote:
Just a reminder that this old thread is not yet resolved and
currently I'm essentially stuck.
I hope somebody who has a clue will answer your email.
I still have various important markers on this mail thread, to see if
I can tell something about it, but I did not manage to pick it up again.
It will happen really soon now ...
drop_semicolons
I’ve applied and push your first change.
As for semicolon, the standard style is rather to put them, not to
drop them.
Strictly speaking there is no standard for semicolons in Isabelle/ML,
only the universal standard of uniformity: a file either has extra
semicolons or does not have extra semicolons.
More than 20 years ago, semicolons where generally en-vogue, and no
surprise for me in SML. Then they became less popular, e.g. in Scala we
now see sophisticated rules for implicit semicolon inference. The
Isar language has lost its semicolon altogether some weeks ago
(5ff61774df11).
Over the decades I have occasionally experimented with writing less
semicolons in ML, but each time I ran into practical inconveniences
concerning error situations (broken partial input), and closed ML
modules versus open sequences of declarations (e.g. in the 'ML' command).
My present style of doing it (approx. the last 10 years) is somehow
optimized in that respect. Whenever I do serious renovations on some
old ML module, I first normalize the semicolon style (and other styles
as well), just to save a lot of time in the actual work.
Makarius
# HG changeset patch
# Parent 2538b2c51769f9e40c424644233f8f8c5cb6eac3
apply type-unifier before inserting variants
diff -r 2538b2c51769 -r 790518068cc2 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.MLTue Jan 27 16:12:40 2015 +0100
+++ b/src/Tools/adhoc_overloading.MLWed Jan 28 13:18:46 2015 +0100
@@ -62,7 +62,7 @@
structure Overload_Data = Generic_Data
(
type T =
-{variants : (term * typ) list Symtab.table,
+{variants : (term * typ) list Symtab.table, (*store type to avoid repeated
fastype_of*)
oconsts : string Termtab.table};
val empty = {variants = Symtab.empty, oconsts = Termtab.empty};
val extend = I;
@@ -84,6 +84,8 @@
Overload_Data.map (fn {variants = vtab, oconsts = otab} =
{variants = f vtab, oconsts = g otab});
+val dummify_types = map_types (K dummyT)
+
val is_overloaded = Symtab.defined o #variants o Overload_Data.get o
Context.Proof;
val get_variants = Symtab.lookup o #variants o Overload_Data.get o
Context.Proof;
val get_overloaded = Termtab.lookup o #oconsts o Overload_Data.get o
Context.Proof;
@@ -99,10 +101,11 @@
val remove_variants =
(case get_variants (Context.proof_of context) oconst of
NONE = I
- | SOME vs = fold (Termtab.remove (op =) o rpair oconst o fst) vs);
+ | SOME vs = fold (Termtab.remove (op =) o rpair oconst o
dummify_types o fst) vs);
in map_tables (Symtab.delete_safe oconst) remove_variants context end;
in
-if is_overloaded (Context.proof_of context) oconst then
remove_oconst_and_variants context oconst
+if is_overloaded (Context.proof_of context) oconst then
+ remove_oconst_and_variants context oconst
else err_not_overloaded oconst
end;
@@ -110,9 +113,9 @@
fun generic_variant add oconst t context =
let
val ctxt = Context.proof_of context;
- val _ = if is_overloaded ctxt oconst then () else err_not_overloaded
oconst;
- val T = t | fastype_of;
- val t' = Term.map_types (K dummyT) t;
+ val _ = is_overloaded ctxt oconst orelse err_not_overloaded oconst;
+ val t_T = (t, fastype_of t);
+ val t' = dummify_types t;
in
if add then
let
@@ -121,16 +124,15 @@
NONE = ()
| SOME oconst' = err_duplicate_variant oconst');
in
- map_tables (Symtab.cons_list (oconst, (t', T))) (Termtab.update (t',
oconst)) context
+ map_tables (Symtab.cons_list (oconst, t_T)) (Termtab.update (t',
oconst)) context
end
else
let
- val _ =
-if member variants_eq (the (get_variants ctxt oconst)) (t', T)
then ()
-else err_not_a_variant oconst;
+ val _ = member variants_eq (the (get_variants ctxt oconst)) t_T
orelse
+err_not_a_variant oconst;
in
-
Re: [isabelle-dev] Lexical structure of ML strings
I think the following thread is related to your question: http://comments.gmane.org/gmane.science.mathematics.logic.isabelle.user/10007 On 01/26/2015 09:30 AM, Florian Haftmann wrote: I have some doubt whether the parsing of strings by Isabelle/ML conforms to plain ML. See the following examples. ML_val ‹ val s = a\nb; writeln s; › OK, seems quite plausible. ML_val ‹ val s = a\\b; writeln s; › OK, seems quite plausible. ML_val ‹ val s = a\\^isub1; writeln s; › This gives a lexical error, though I guess it should interpret as plain a\^isub1. (Alas I have no suitable literature at hand which would give an exact specification of a string's lexical structure in ML). So, is this the intended behaviour? I have stumbled over that issue while trying to generate code involvings strings of that kind. Any suggestions welcome. Thanks a lot, 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] Isabelle/jEdit: imports
As of c7f6f01ede15 I noticed the following behavior. Suppose I have a theory file with the following content theory Foo imports Main begin end So far so good. Now I add another import. theory Foo imports Main ~~/src/HOL/Tools/Adhoc_Overloading begin end By accident this refers to a non-existent file. Instead of a corresponding error-message, however, the whole file maintains a lightly red background and doesn't seem to be processed at all (i.e., I do not get any output if I edit in between begin and end). cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] adhoc overloading: ugly output
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
Re: [isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading
Just a reminder that this old thread is not yet resolved and currently
I'm essentially stuck.
Independent of my being stuck, could one of the devs apply at least the
first of the following attached patches (and the second one depending on
whether dropping semicolons is in general seen as good style or not)
that somehow drowned in previous emails:
delete
drop_semicolons
cheers
chris
On 12/01/2014 01:56 PM, Christian Sternagel wrote:
Thanks for the valuable pointers Florian!
As far as I understand, type inference is a necessary prerequisite for
expand_abbrevs (so that afterwards matching and instantiating by the
obtained substitution suffice for getting the proper type).
Two thoughts:
1) I wouldn't want to add yet another layer of type-inference directly
before the adhoc_overloading check. Anyway, currently it doesn't even
seem possible to inject something after type inference but before
expand_abbrevs.
2) Even if full type inference was done before the adhoc_overloading
check is executed, matching alone wouldn't suffice.
The reason for 2 is that often (adhoc) overloaded constants have a very
general type (which can't be made more specific while still supporting
all desired variants). Consider e.g. monadic bind, whose type is 'a
= ('b = 'c) = 'd or pure :: 'a = 'b from Andreas' example. More
specifically, for the term pure id type inference will infer type 'b
while the corresponding id has type 'a = 'a and this instance of
pure has type ('a = 'a) = 'b. Thus there is no connection between
the domain- and range-type of pure whatsoever. Now the type of
pure_stream :: 'a1 = 'a1 stream cannot be instantiated to ('a = 'a)
= 'b. Only via unification we can find that with
['a1 - ('a = 'a), b' - ('a = 'a) stream]
we actually can insert pure_stream here. The problem (I think) is that
by unification we might inject schematic type variables that stem from
types of variants (like 'a1 above). Into the ongoing check phase whose
context doesn't know about them.
Thus again my questions. Does this seem plausible? And is there a way to
turn such alien schematic type variables into known ones?
cheers
chris
On 11/27/2014 08:50 AM, Florian Haftmann wrote:
Hi Christian,
I'm mostly guessing here. Maybe somebody with deeper knowledge of the
system could comment whether this would be feasible (and also the right
way to go).
I have not spent much thought on the code, but tried to take a bird's
perspective.
The whole matter is about overloaded abbreviations. Hence, it's about
abbreviation expansion intermingled with type inference.
Having a look syntax_phases.ML
(* standard phases *)
val _ = Context.
(typ_check 0 standard Proof_Context.standard_typ_check #
term_check 0 standard
(fn ctxt = Type_Infer_Context.infer_types ctxt # map
(Proof_Context.expand_abbrevs ctxt)) #
term_check 100 standard_finish
Proof_Context.standard_term_check_finish #
term_uncheck 0 standard Proof_Context.standard_term_uncheck);
I see that type inference and abbreviation expansion occur on the same
term check level. Hence the overloading mechanisms could go here.
Proof_Context.expand_abbrevs essentially boils down to Consts.certify.
Maybe a comparision of these with the current implementation of
adhoc-overloading can give some clues.
Cheers,
Florian
# HG changeset patch
# Parent be4a911aca712cc928d1f798488205ce7c5fac92
typo in description
diff -r be4a911aca71 -r f653343d16ba src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.MLWed Nov 19 19:12:14 2014 +0100
+++ b/src/Tools/adhoc_overloading.MLFri Nov 21 19:58:22 2014 +0100
@@ -239,7 +239,7 @@
val _ =
Outer_Syntax.local_theory @{command_spec no_adhoc_overloading}
-add adhoc overloading for constants / fixed variables
+delete adhoc overloading for constants / fixed variables
(Parse.and_list1 (Parse.const -- Scan.repeat Parse.term)
adhoc_overloading_cmd false);
end;
# HG changeset patch
# Parent 2b1505ca7ff4d324e4c595374c97fdcc8e4769bb
drop superfluous semicolons
diff -r 2b1505ca7ff4 -r 941653538854 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.MLSun Nov 23 20:07:19 2014 +0100
+++ b/src/Tools/adhoc_overloading.MLSun Nov 23 20:09:38 2014 +0100
@@ -19,19 +19,19 @@
structure Adhoc_Overloading: ADHOC_OVERLOADING =
struct
-val show_variants = Attrib.setup_config_bool @{binding show_variants} (K
false);
+val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false)
(* errors *)
fun err_duplicate_variant oconst =
- error (Duplicate variant of ^ quote oconst);
+ error (Duplicate variant of ^ quote oconst)
fun err_not_a_variant oconst =
- error (Not a variant of ^ quote oconst);
+ error (Not a variant of ^ quote oconst)
fun err_not_overloaded oconst =
- error (Constant ^ quote oconst ^ is not declared as overloaded);
+ error (Constant ^ quote oconst ^ is not declared as overloaded)
fun err_unresolved_overloading ctxt0 (c, T) t
[isabelle-dev] BNF: number of dead variables
Dear BNF gurus, is there a reliable way to check - given the name of a type constructor - how many dead type parameters it has? I tried (case BNF_FP_Def_Sugar.fp_sugar_of lthy tname of SOME sugar = if BNF_Def.dead_of_bnf (#fp_bnf sugar) 0 then error ... ... However having something like datatype foo = Foo | Bar I noticed that print_bnfs does not list type foo, what is worse, the above check apparently yields a number greater than 0 for foo, since the corresponding error is triggered. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] BNF: number of dead variables
Hi Jasmin, thanks for the quick reply. Your suggestion works fine! cheers chris On 12/03/2014 03:46 PM, Jasmin Christian Blanchette wrote: Hi Chris, is there a reliable way to check - given the name of a type constructor - how many dead type parameters it has? I tried (case BNF_FP_Def_Sugar.fp_sugar_of lthy tname of SOME sugar = if BNF_Def.dead_of_bnf (#fp_bnf sugar) 0 then error ... ... However having something like datatype foo = Foo | Bar I noticed that print_bnfs does not list type foo, It doesn't because it's a nullary BNF and all types are trivially nullary BNFs, so there's no point in storing this pointless information in our databases. Instead, we store only a single such type, namely 'a, where 'a is dead. This BNF is called DEADID -- it's listed when you execute print_bnfs, and you can grep for it in src/HOL/*.thy to find out where it is registered. So when you look up foo, you get, somewhat confusingly, the BNF entry for 'a. A more reliable way to count the number of deads is to use the equation: num_dead_vars = num_type_vars - num_live_vars BNF_Def.live_of_bnf and Sign.arity_number are your friends. I hope this solves your problem. Don't hesitate to let us know if you run into issues again. Those interfaces were never very polished, nor documented (although I might come to add a section to isabelle doc datatypes about the ML functions -- there is an embryonic, commented out Using the Standard ML Interface section already). Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle/PIDE as ML IDE: syntax highlighting of string literals
Dear Makarius, nowadays I'm doing all my ML coding in Isabelle/PIDE, which is really nice to use by the way. A tiny thing I noticed recently is that in the presence of control symbols, string literals are highlighted somewhat strange. To see what I mean, consult the attached screenshot, where after a \^sub in a string literal function names are no longer highlighted black. cheers chris On 11/17/2014 09:46 PM, Makarius wrote: Dear Isabelle users, the current Isabelle2014 has this built-in PIDE support for official Standard ML (SML'97) that was already mentioned a few times before; it is briefly explained in the NEWS of the distribution. I would like to publicize this as much as possible. It could help the general cause of Standard ML (the best unknown programming language in the world) and in particular Poly/ML (the best unknown implementation of SML). Here is the corresponding entry on my new website/blog: http://sketis.net/?p=103 This is a permanent link that can be used elsewhere, despite the slightly odd name, which is normal in WordPress, I think. Of course, enthusiastic users are encouraged to publish their own texts about the SML IDE. My blog mentions a sister entry on Stackoverflow: http://stackoverflow.com/questions/2036744/ml-ide-and-compiler-for-windows-or-linux-or-mac I don't want to bribe anybody, but maybe we could collect a few more votes for that article so that it is higher ranked. This is relevant, because Google presently places it first for a query like SML IDE. Makarius http://stop-ttip.org 906,830 people so far ___ 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
Thanks again Dmitriy,
it seems that my fix was too quick. Since sending my email yesterday I
worried already whether doing unification inside adhoc_overloading.ML is
such a good idea (since the unifier might inject schematic type
variables stemming from the internal generic theory data of adhoc
overloading into the ongoing check-phase). Apparently it isn't.
Is there a way to turn arbitrary schematic type variables into ones that
will not cause problems during type-inference? If so, it might be better
to just check for unifiability and then inject a variant v with its
most general type but where polymorphic variables are made known to
the context.
I'm mostly guessing here. Maybe somebody with deeper knowledge of the
system could comment whether this would be feasible (and also the right
way to go).
cheers
chris
On 11/24/2014 09:03 AM, Dmitriy Traytel wrote:
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
Re: [isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading
*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 problems while matching.
Why, however 'c is produced instead of 'b is not immediately clear
to me. I'll investigate.
cheers
chris
[isabelle-dev] BNF: dead or alive?
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)
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?).
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)?.
cheers
chris
Maybe unrelated: The datatype declaration
datatype (dead 'a, 'b) dlist = DNil | DCons 'a 'b ('a, 'b) dlist
work, but
datatype (dead 'a, 'b) dlist = DNil | DCons 'a × 'b ('a, 'b) dlist
results in an internal tactic failure.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] BNF: dead or alive?
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? cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Abbreviations and find_theorems
Hi Florian, many month ago I was also surprised, then annoyed, and then I got used to always adding the underscore-argument. I fully agree that users shouldn't have to worry about such technicalities. cheers chris On 11/15/2014 05:58 PM, Florian Haftmann wrote: Hi all, when searching for theorems, abbreviations may behave surprisingly: find_theorems odd _ -- ‹considerable results› find_theorems odd -- ‹no results› I guess this is due to abbreviation expansion which then yields find_theorems λa. odd a -- ‹no results› So, this is formally correct but nevertheless IMHO inconventiently. May naive expectation is that when I am searching for a particular operations I do not that to think about such technical detail. What do others think? This refers to 059ba950a657. Cheers, 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] [isabelle] Theory Prefix_Order
(moved from isabelle-users since I'm referring to the development versions of Isabelle and the AFP below) Dear Julian, unexpectedly I found some time to have a look earlier. First, the naming layer provided by the lemmas statements in Prefix_Order is there to keep compatibility with some AFP entries. (There are mainly two naming schemes around, either Peq P for weak and strict part of an order or P and strict_P for the same; and Sublist uses the former, while some AFP entries use the latter.) I think (without trying, however) your suggested changes would break some AFP entries. Instead I suggest the attached changes (the order of patches is to be found in series) which are tested against Isabelle: 9239a33935c6 and AFP: 42be0138cfe5 Thanks for spotting this. cheers chris On 10/20/2014 05:00 PM, Julian Brunner wrote: Dear all, I've stumbled upon a few issues with the theory Library/Prefix_Order.thy. This theory instantiates the order type class for lists like this: definition (xs::'a list) = ys == prefixeq xs ys definition (xs::'a list) ys == xs = ys Not (ys = xs) It then goes on to lift theorems about the constants 'prefixeq' and 'prefix' to the constants 'op =' and 'op ', adding simp/intro/elim attributes in the process. However, a few things seem to have gone wrong here. First off, we have: lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def] lemmas strict_prefixI [intro?] = prefixI [folded less_list_def] The first line hides the fact Sublist.prefixI, so the theorem declared in the second line is just a duplicate of the one in the first and the 'folded less_list_def' attribute is applied in vain. However, even when using the fully qualified fact Sublist.prefixI, it doesn't work the way I assume it was intended to, since 'op ' is not defined in terms of 'prefix', so the 'folded less_list_def' attribute still doesn't apply. Attached are my attempts at fixing these and a few other issues. Please let me know if I should have posted this on the developer mailing list. Cheers, Julian # HG changeset patch # Parent d5b36d47d92dfbeebeb5f2e86889296cabdbc457 dropped duplicate fact diff -r d5b36d47d92d -r 1541b682d41d src/HOL/Library/Sublist.thy --- a/src/HOL/Library/Sublist.thy Tue Oct 21 14:27:28 2014 +0200 +++ b/src/HOL/Library/Sublist.thy Tue Oct 21 14:30:02 2014 +0200 @@ -396,29 +396,6 @@ lemma suffixeq_take: suffixeq xs ys \Longrightarrow ys = take (length ys - length xs) ys @ xs by (auto elim!: suffixeqE) -lemma suffixeq_suffix_reflclp_conv: suffixeq = suffix\^sup=\^sup= -proof (intro ext iffI) - fix xs ys :: 'a list - assume suffixeq xs ys - show suffix\^sup=\^sup= xs ys - proof -assume xs \noteq ys -with `suffixeq xs ys` show suffix xs ys - by (auto simp: suffixeq_def suffix_def) - qed -next - fix xs ys :: 'a list - assume suffix\^sup=\^sup= xs ys - then show suffixeq xs ys - proof -assume suffix xs ys then show suffixeq xs ys - by (rule suffix_imp_suffixeq) - next -assume xs = ys then show suffixeq xs ys - by (auto simp: suffixeq_def) - qed -qed - lemma suffix_reflclp_conv: suffix\^sup=\^sup= = suffixeq by (intro ext) (auto simp: suffixeq_def suffix_def) @@ -508,7 +485,7 @@ lemma list_emb_suffixeq: assumes list_emb P xs ys and suffixeq ys zs shows list_emb P xs zs - using assms and list_emb_suffix unfolding suffixeq_suffix_reflclp_conv by auto + using assms and list_emb_suffix unfolding suffix_reflclp_conv [symmetric] by auto lemma list_emb_length: list_emb P xs ys \Longrightarrow length xs \le length ys by (induct rule: list_emb.induct) auto # HG changeset patch # Parent e8ecc79aee432d084a1539f69bb95a656f4140fd move facts about parallel to corresponding document section diff -r e8ecc79aee43 -r d5b36d47d92d src/HOL/Library/Sublist.thy --- a/src/HOL/Library/Sublist.thy Mon Oct 20 18:33:14 2014 +0200 +++ b/src/HOL/Library/Sublist.thy Tue Oct 21 14:27:28 2014 +0200 @@ -261,6 +261,46 @@ lemma parallel_commute: a \parallel b \longleftrightarrow b \parallel a unfolding parallel_def by auto +lemma parallelD1: x \parallel y \Longrightarrow \not prefixeq x y + by blast + +lemma parallelD2: x \parallel y \Longrightarrow \not prefixeq y x + by blast + +lemma parallel_Nil1 [simp]: \not x \parallel [] + unfolding parallel_def by simp + +lemma parallel_Nil2 [simp]: \not [] \parallel x + unfolding parallel_def by simp + +lemma Cons_parallelI1: a \noteq b \Longrightarrow a # as \parallel b # bs + by auto + +lemma Cons_parallelI2: \lbrakk a = b; as \parallel bs \rbrakk \Longrightarrow a # as \parallel b # bs + by (metis Cons_prefixeq_Cons parallelE parallelI) + +lemma not_equal_is_parallel: + assumes neq: xs \noteq ys +and len: length xs = length ys + shows xs \parallel ys + using len neq +proof (induct rule: list_induct2) + case Nil + then show ?case by simp +next + case (Cons a as b bs) + have ih: as \noteq bs \Longrightarrow as \parallel bs by fact +
Re: [isabelle-dev] [isabelle] Imperative_HOL: code generator setup for Haskell
moved from isabelle-users
*
Dear all,
In the attached theory files I tried to follow the let Haskell moan if
it is not linear approach. And on first sight it seems to work.
My motivation is to be able to use imperative code inside pure functions
(in the sense that the result type is not 'a Heap). E.g., for
IsaFoR/CeTA it would be unrealistic to change the result type of all our
check-functions into 'a Heap for some 'a, just to be able, to use,
e.g., more efficient unification via union-find with arrays.
What I did in the attached theory files is essentially make a copy of
the Imperative/HOL development using 'a Heap and adding an additional
phantom type parameter 's (for state) *everywhere* (i.e., heap monad,
array type and operations, ref type and operations, ...). Finally there
is a function runST :: (unit, 'a) st = 'a (where ('s, 'a) st more
or less corresponds to the previous 'a Heap) which is code generated
to Haskell's runST :: (forall s. ST s a) - a. It's logical definition
is runST c = (case execute c initial_state of Some (x, _) = x) where
initial_state is State ST_Heap.empty for the new datatypes
's state = State (heap : heap) (*heap is almost the same as the
original heap)
and
(dead 's, 'a) st = ST (execute : 's state = ('a * 's state) option)
Of course this approach only works for Haskell (more specifically for
compilers that support rank-2 types).
I guess the previous Imperative/HOL could be regained by instantiating
's to some concrete RealWorld token.
What do you think?
cheers
chris
On 10/07/2014 05:52 PM, Florian Haftmann wrote:
2) How would we actually use an imperative function from inside some
pure function? Can
there be a mapping to runST for Haskell (I guess that would not be
safe, since there's no
rank-2 types in Isabelle/HOL)? Any thoughts or further explanations?
With the current setup, you cannot. If you look at the code_printing
declarations in Heap_Monad, you will see that the heap type is mapped to
ST RealWorld. That means that heap values are meant to be used with
stToIO rather than runST.
[...]
That is, if you nevertheless serialise a function that
returns a reference, Haskell's type system should prevent you from
applying runST to it. Hence, you can generate code that does not compile
afterwards. From the point of view on partial correctness, this is sound.
Initially I have been so optimistic to follow that »let Haskell moan if
it is not linear« approach, but there have been technical problems which
could not been solved within the existing infrastructure. The details I
do not remember, but maybe the hg history knows more.
Florian
ST.tgz
Description: application/compressed-tar
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] rtrancl lemma proposal
Dear developers, the following lemma seems like a basic fact about rtrancl: lemma rtrancl_map: assumes ⋀x y. (x, y) ∈ r ⟹ (f x, f y) ∈ s and (x, y) ∈ r⇧* shows (f x, f y) ∈ s⇧* using assms(2, 1) by (induct) (auto intro: rtrancl.rtrancl_into_rtrancl) I didn't find it in Main. Did anybody else ever use/need it? Is it already part of some theory I did overlook? How about adding it? Caveat: It seems to be necessary to strongly instantiate it before usage. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Imperative HOL: typo?
I moved this thread from isabelle-users to isabelle-dev. (Please let me know in case this was the wrong call.) Dear all, I tried the variant of the lemma from my previous mail and the result is in the attached patch (created with hg qnew). For testing I ran isabelle build -b HOL-Imperative_HOL as well as isabelle afp_build Separation_Logic_Imperative_HOL as far as I can tell the only session in the AFP depending on Imperative_HOL. I did not obtain any errors. cheers chris On 09/26/2014 01:00 PM, Christian Sternagel wrote: Dear Florian, I will check your proposal. However, I was more confused by the first premise of successE referring to f while afterwards the command is sometimes referred to by c. Shouldn't it be the same (either f or c) throughout the lemma? lemma successE: assumes success f h obtains r h' where execute f h = Some (r, h') using assms by (auto simp: success_def) shouldn't that imply the other two equations? cheers chris On 09/15/2014 08:59 PM, Florian Haftmann wrote: Hi Christian, Is the c in the following lemma (to be found in ~~/src/HOL/Imperative_HOL/Heap_Monad.thy) seems strange: lemma successE: assumes success f h obtains r h' where r = fst (the (execute c h)) and h' = snd (the (execute c h)) and execute f h ≠ None using assms by (simp add: success_def) Strange, indeed, particularly since the first two obtained claused are essentially definitional tautologies. Maybe this would suite better: lemma successE: assumes success f h obtains r h' where r = fst (the (execute c h)) and h' = snd (the (execute c h)) and execute f h = Some (r, h') using assms by (simp add: success_def) There are actually some proofs using successE. How do they perform with this lemma definition changed? Florian cheers chris # HG changeset patch # Parent 126c353540fc081be30ce08a10c14f9d8da332f6 tuned Heap_Monad.successE diff -r 126c353540fc -r 9a54096ae0af src/HOL/Imperative_HOL/Array.thy --- a/src/HOL/Imperative_HOL/Array.thy Fri Sep 26 09:58:35 2014 +0200 +++ b/src/HOL/Imperative_HOL/Array.thy Fri Sep 26 14:05:14 2014 +0200 @@ -255,8 +255,7 @@ lemma effect_nthE [effect_elims]: assumes effect (nth a i) h h' r obtains i length h a r = get h a ! i h' = h - using assms by (rule effectE) -(erule successE, cases i length h a, simp_all add: execute_simps) + using assms by (rule effectE) (cases i length h a, auto simp: execute_simps elim: successE) lemma execute_upd [execute_simps]: i length h a \Longrightarrow @@ -276,8 +275,7 @@ lemma effect_updE [effect_elims]: assumes effect (upd i v a) h h' r obtains r = a h' = update a i v h i length h a - using assms by (rule effectE) -(erule successE, cases i length h a, simp_all add: execute_simps) + using assms by (rule effectE) (cases i length h a, auto simp: execute_simps elim: successE) lemma execute_map_entry [execute_simps]: i length h a \Longrightarrow @@ -298,8 +296,7 @@ lemma effect_map_entryE [effect_elims]: assumes effect (map_entry i f a) h h' r obtains r = a h' = update a i (f (get h a ! i)) h i length h a - using assms by (rule effectE) -(erule successE, cases i length h a, simp_all add: execute_simps) + using assms by (rule effectE) (cases i length h a, auto simp: execute_simps elim: successE) lemma execute_swap [execute_simps]: i length h a \Longrightarrow @@ -320,8 +317,7 @@ lemma effect_swapE [effect_elims]: assumes effect (swap i x a) h h' r obtains r = get h a ! i h' = update a i x h i length h a - using assms by (rule effectE) -(erule successE, cases i length h a, simp_all add: execute_simps) + using assms by (rule effectE) (cases i length h a, auto simp: execute_simps elim: successE) lemma execute_freeze [execute_simps]: execute (freeze a) h = Some (get h a, h) diff -r 126c353540fc -r 9a54096ae0af src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Sep 26 09:58:35 2014 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Sep 26 14:05:14 2014 +0200 @@ -82,10 +82,8 @@ lemma successE: assumes success f h - obtains r h' where r = fst (the (execute c h)) -and h' = snd (the (execute c h)) -and execute f h \noteq None - using assms by (simp add: success_def) + obtains r h' where execute f h = Some (r, h') + using assms by (auto simp: success_def) named_theorems success_intros introduction rules for success @@ -266,11 +264,11 @@ lemma execute_bind_success: success f h \Longrightarrow execute (f \guillemotright= g) h = execute (g (fst (the (execute f h (snd (the (execute f h))) - by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def) + by (cases f h rule: Heap_cases) (auto elim: successE simp add: bind_def) lemma success_bind_executeI: execute f h = Some (x, h') \Longrightarrow success (g x) h' \Longrightarrow success (f \guillemotright= g) h - by (auto intro!: successI
[isabelle-dev] duplicate fact in List
Dear all, just an observation. The facts List.drop_Suc_conv_tl: ?i length ?xs ⟹ ?xs ! ?i # drop (Suc ?i) ?xs = drop ?i ?xs List.nth_drop': ?i length ?xs ⟹ ?xs ! ?i # drop (Suc ?i) ?xs = drop ?i ?xs are duplicates of each other. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] default cases rule
Dear all,
routinely checking IsaFoR against the development version of Isabelle
(more precisely d0dffec0da2b) I stumbled across the following
proof-breaking inconvenience:
In Isabelle2014 and earlier we could do
notepad
begin
fix p :: ('a × 'b × 'c) and xs
assume p ∈ set xs
then obtain x y z where (x, y, z) ∈ set xs
by (cases p) auto
end
i.e., relying on the default cases rule the proof went through.
In the development version, however, the following subgoals remain after
apply (cases p)
goal (2 subgoals):
1. ⋀z2. (⋀x y z. (x, y, z) ∈ set xs ⟹ thesis) ⟹
xs = p # z2 ⟹ thesis
2. ⋀z1 z2.
(⋀x y z. (x, y, z) ∈ set xs ⟹ thesis) ⟹
xs = z1 # z2 ⟹ p ∈ set z2 ⟹ thesis
That is, the default rule changed for assumptions of the form _ : set _.
First question: is this intentional and what is the current default rule?
Second question: is it considered bad form to rely on default rules?
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] default cases rule
Thanks for your replies! I forgot to check the NEWS ;) For the record: the change affected in the order of 10 proofs in IsaFoR (most of which unnecessarily chained facts into the cases method) which where of course trivially repaired. cheers chris On 09/05/2014 02:48 PM, Jasmin Christian Blanchette wrote: Hi all, Dmitriy wrote: 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. I would like to add that this radical change broke only a handful of proofs in the AFP, i.e., it was not so radical after all. ;) Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] pull request (HOL-Library/Sublist(_Order))
Thanks! I'll take care of the AFP now. -cheers chris On 07/03/2014 02:41 PM, Florian Haftmann wrote: Hi Christian, see now http://isabelle.in.tum.de/repos/isabelle/rev/b69a1272cb04 Cheers, Florian On 30.06.2014 15:59, Christian Sternagel wrote: Dear developers, would somebody be willing to pull in the attached patches into HOL/Library? The patches where generated with the help of mercurial's mq extension (i.e., the series file gives the order of application) and each patch can be imported into a repository by hg import --user Christian Sternagel patch-file In the AFP the attached changes do only influence my entry Well-Quasi-Orders and (to a tiny amount) Myhill-Nerode, for which I have corresponding patches in my local AFP repo. The intention behind the patches is as follows: * No built-in reflexivity for list embedding. Which is more standard in the literature. Then reflexivity of list embedding depends on the reflexivity of the given relation on elements. * To make this more obvious remove eq suffix from list_hembeq. Plus, to obtain a slightly shorter (and as I think, more easy to parse) name, rename list_hembeq into list_emb (ideally this should be List.emb at some point). * Added monotonicity lemma for list_emb which is needed for inductive definitions based on it. * Weaker assumption for transitivity lemma of list_emb. * Added lemma that for a list that is embedded in another one, i.e., list_emb P xs ys, all its elements are in the given base relation P with some element of the latter, i.e., ALL x : set xs. EX y : set ys. P x y. 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
[isabelle-dev] pull request (HOL-Library/Sublist(_Order))
Dear developers,
would somebody be willing to pull in the attached patches into
HOL/Library? The patches where generated with the help of mercurial's mq
extension (i.e., the series file gives the order of application) and
each patch can be imported into a repository by
hg import --user Christian Sternagel patch-file
In the AFP the attached changes do only influence my entry
Well-Quasi-Orders and (to a tiny amount) Myhill-Nerode, for which I have
corresponding patches in my local AFP repo.
The intention behind the patches is as follows:
* No built-in reflexivity for list embedding. Which is more standard in
the literature. Then reflexivity of list embedding depends on the
reflexivity of the given relation on elements.
* To make this more obvious remove eq suffix from list_hembeq. Plus,
to obtain a slightly shorter (and as I think, more easy to parse) name,
rename list_hembeq into list_emb (ideally this should be List.emb
at some point).
* Added monotonicity lemma for list_emb which is needed for inductive
definitions based on it.
* Weaker assumption for transitivity lemma of list_emb.
* Added lemma that for a list that is embedded in another one, i.e.,
list_emb P xs ys, all its elements are in the given base relation P
with some element of the latter, i.e., ALL x : set xs. EX y : set ys. P
x y.
cheers
chris
# HG changeset patch
# Parent 48c582067cb9a6551b85710ea9cf51158cd2e5b9
weaker assumption for list_emb_trans; added lemma
diff -r 48c582067cb9 -r d2e2e72eb1a0 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy Thu Jun 26 13:24:41 2014 +0200
+++ b/src/HOL/Library/Sublist.thy Thu Jun 26 15:31:04 2014 +0200
@@ -514,34 +514,31 @@
by (induct rule: list_emb.induct) auto
lemma list_emb_trans:
- assumes \Andx y z. \lbrakkx \in A; y \in A; z \in A; P x y; P y
z\rbrakk \Longrightarrow P x z
- shows \Andxs ys zs. \lbrakkxs \in lists A; ys \in lists A; zs \in
lists A;
-list_emb P xs ys; list_emb P ys zs\rbrakk \Longrightarrow list_emb P
xs zs
+ assumes \Andx y z. \lbrakkx \in set xs; y \in set ys; z \in set
zs; P x y; P y z\rbrakk \Longrightarrow P x z
+ shows \lbrakklist_emb P xs ys; list_emb P ys zs\rbrakk
\Longrightarrow list_emb P xs zs
proof -
- fix xs ys zs
assume list_emb P xs ys and list_emb P ys zs
-and xs \in lists A and ys \in lists A and zs \in lists A
- then show list_emb P xs zs
+ then show list_emb P xs zs using assms
proof (induction arbitrary: zs)
case list_emb_Nil show ?case by blast
next
case (list_emb_Cons xs ys y)
from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
- where zs: zs = us @ v # vs and P y v and list_emb P ys vs by blast
+ where zs: zs = us @ v # vs and P\^sup=\^sup= y v and list_emb P
ys vs by blast
then have list_emb P ys (v#vs) by blast
then have list_emb P ys zs unfolding zs by (rule list_emb_append2)
-from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by simp
+from list_emb_Cons.IH [OF this] and list_emb_Cons.prems show ?case by auto
next
case (list_emb_Cons2 x y xs ys)
from list_emb_ConsD [OF `list_emb P (y#ys) zs`] obtain us v vs
where zs: zs = us @ v # vs and P y v and list_emb P ys vs by blast
-with list_emb_Cons2 have list_emb P xs vs by simp
+with list_emb_Cons2 have list_emb P xs vs by auto
moreover have P x v
proof -
- from zs and `zs \in lists A` have v \in A by auto
- moreover have x \in A and y \in A using list_emb_Cons2 by
simp_all
+ from zs have v \in set zs by auto
+ moreover have x \in set (x#xs) and y \in set (y#ys) by simp_all
ultimately show ?thesis
-using `P x y` and `P y v` and assms
+using `P x y` and `P y v` and list_emb_Cons2
by blast
qed
ultimately have list_emb P (x#xs) (v#vs) by blast
@@ -549,6 +546,11 @@
qed
qed
+lemma list_emb_set:
+ assumes list_emb P xs ys and x \in set xs
+ obtains y where y \in set ys and P x y
+ using assms by (induct) auto
+
subsection {* Sublists (special case of homeomorphic embedding) *}
@@ -607,7 +609,7 @@
qed
lemma sublisteq_trans: sublisteq xs ys \Longrightarrow sublisteq ys zs
\Longrightarrow sublisteq xs zs
- by (rule list_emb_trans [of UNIV op =]) auto
+ by (rule list_emb_trans [of _ _ _ op =]) auto
lemma sublisteq_append_le_same_iff: sublisteq (xs @ ys) ys
\longleftrightarrow xs = []
by (auto dest: list_emb_length)
# HG changeset patch
# Parent fc4d65afdf136a1d54bbd7419aede9cf70defcff
renamed list_hembeq into slightly shorter list_emb
diff -r fc4d65afdf13 -r f07fe64d9f21 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy Mon Jun 23 12:54:48 2014 +0200
+++ b/src/HOL/Library/Sublist.thy Thu Jun 26 13:15:21 2014 +0200
@@ -428,115 +428,115 @@
subsection {* Homeomorphic embedding on lists *}
-inductive list_hembeq :: ('a \Rightarrow 'a \Rightarrow bool)
\Rightarrow 'a list \Rightarrow 'a list \Rightarrow
[isabelle-dev] lemma
Dear all, how about adding the following lemmas to the order class? lemma (in order) rtranclp_less_eq [simp]: (op ≤)⇧*⇧* = op ≤ by (intro ext) (auto elim: rtranclp_induct) lemma (in order) tranclp_less [simp]: (op )⇧+⇧+ = op by (intro ext) (auto elim: tranclp_induct) lemma (in order) rtranclp_greater_eq [simp]: (op ≥)⇧*⇧* = op ≥ by (intro ext) (auto elim: rtranclp_induct) lemma (in order) tranclp_greater [simp]: (op )⇧+⇧+ = op by (intro ext) (auto elim: tranclp_induct) cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] html output of theories
On 04/14/2014 12:01 PM, Makarius wrote: So what are the characteristic points for theory presentation, either (1) as paginated PDF, (2) as static HTML, (3) as dynamic document within the Prover IDE? I hope I got it right that you are interested in opinions here? Otherwise, sorry ;) (1) I think this is most important for using Isabelle when typesetting a paper. At the moment I do either of two things: - Use a theory Snippets.thy that just recapitulates some existing definitions/lemmas/... and generate latex snippets to be included in my paper (mostly when working together with researchers that are not using Isabelle themselves). Or - use a theory Paper.thy whose corresponding paginated PDF *is* my paper. (2) I mostly use HTML for browsing Isabelle theories. But at the moment this is not very comfortable (no links from constants to their definition, nor from lemma names to the corresponding lemma, ...). However this is all there in Isabelle/jEdit. And my only reason for not using Isabelle/jEdit for the above purpose is that I have to wait until everything is loaded, whereas somebody else already generated the HTML for HOL/Library, AFP, etc. I also agree that HTML output is important for people who don't know Isabelle yet. (3) This is what we all use every day, right? So this should be most sophisticated (and already is, I think). Presentation wise the only negative point I can think of, is that ugly LaTeX code is mostly unreadable in the theory-file, while I need it sometimes for (1). In that respect it would be wonderful if either Isabelle/jEdit would magically present the result of TeXing or support nicely rendered syntax for formatting (I think there is no way around LaTeX when it comes to rendering formulas. Maybe there is. Do you know MathML?). cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: interactive simplifier trace
Dear Lars, today I first tried using the new simplifier tracing facility (within Isabelle/jEdit). I just started but have already some questions ;) In the Simplifier Trace panel itself I did not find out how to get any output. Only after pressing the Show Trace button a new window opens that contains the output. Also in the output, as opposed to [[simp_trace]] I do not see output for recursive calls in conditional rewriting (for the single example I tried). Is there an option to get this? And two general questions (sorry if this is already documented). What is the meaning of Auto update and Auto reply in this panel? cheers chris On 02/04/2014 10:55 AM, Lars Hupel wrote: As of Isabelle/885500f4aa6a: New panel: Simplifier trace. Provides an interactive view of the simplification process, enabled by the newly-introduced simplifier_trace declaration. Note that the previous simp_trace declaration continues to be available. To make use of the new tracing facility, the declaration [[simplifier_trace mode=full]] can be used. It produces (roughly) the same information as the old trace. The trace isn't displayed in the Output panel though, but rather in a Trace window which can be opened via the Show trace button in the Simplifier trace panel. For some more details, refer to the attached user manual (draft). It is an excerpt from my MSc thesis and not yet incorporated into the main Isabelle documentation. ___ 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] adhoc overloading: order inserting overloaded constant
Dear all,
recently I was working a lot with adhoc_overloading. Doing so I often
experienced that my output differed from my input (w.r.t. adhoc
overloading). At that time I did not think too much about it since being
able to input readable formulas was quite enough. But today I suddenly
had an idea what could cause this (to me) strange behavior.
First a minimal example. I introduce a new constant that will be overloaded.
consts F :: 'a ⇒ 'a (FOO)
Then I add a locale and register its fixed constant for adhoc overlaoding:
locale a =
fixes f :: 'a ⇒ 'a
assumes nothing: f x ≡ x
begin
adhoc_overloading
F f
end
Inside this locale I can enter FOO instead of f and f will be
printed as FOO, as I would expect.
Now lets introduce another locale that is built on top of the first one
locale set_a =
elt: a elt_f for elt_f :: 'a ⇒ 'a
begin
adhoc_overloading
F elt_f
definition set_f A = elt_f ` A
adhoc_overloading
F set_f
We now have adhoc overloading for elt_f as well as set_f. For inputting
terms this works as I would expect (i.e., I get an error if it is not
clear from the type which of elt_f and set_f should be inserted for any
given FOO and the corresponding constant, otherwise).
However, as output for
term A (FOO {x. True})
I obtain
A (set_a.set_f FOO {x. True})
while I would have liked to get
A (FOO {x. True})
since this is more readable. Looking at the code of insert_overloaded
inside adhoc_overloading.ML reveals a use of Pattern.rewrite_term,
which seems to do bottom-up rewriting.
So my idea was to instead use top-down rewriting (i.e., first replace
maximal subterms that fit a given pattern). This is what
Pattern.rewrite_term_top does, right? So after replacing
rewrite_term by rewrite_term_top, I get the expected results.
Now my question. Can anybody think of a reason why rewrite_term_top
would not be generally preferable over rewrite_term inside of
insert_overloaded?
If not, could one of the devs incorporate this tiny change please?
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Abbreviations + Monad_Syntax introduce unit itself additional type variable
Reviving this old thread once more ;)
I think I need some clarifications first:
On 12/05/2013 05:05 PM, Florian Haftmann wrote:
Reviving this old thread, Peter and me found out what is actually going
on here.
Basically, nothing wrong. When abbreviations are declared, terms are
checked such that no abbreviations themselves are expanded. So in the
examples, the do-syntax produces an abbreviation bind_do which in this
case is not unfolded and so does not trigger the adhoc-overloading
disambiguation of bind. So, there is nothing wrong here.
Does that also mean that the resulting unit itself is as you would
expect in the following?
abbreviation
abbr2 == do {
Some ();
Some False
} -- additional type variable
Even more, given the analogy that ad-hoc overloading represents some
kind of overloaded abbreviations, adhoc-overloading should never be
expanded while abbreviations are checked (query
Proof_Context.abbrev_mode). @Christian. You might consider to adjust
your code accordingly after a second round of thinking about.
By expanding adhoc overloading do you mean replacing concrete
constants by overloaded generic ones?
When is Proof_Context.abbrev_mode actually true?
What I first thought was that I should avoid to insert overloaded (i.e.,
generic constants; cf. Adhoc_overloading.insert_overloaded) constants
whenever Proof_Context.abbrev_mode is true. But just trying this on some
examples did not change anything (as far as I can tell).
What's the concrete suggestion?
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2013-2 release
Looks good. Sorry for the delay, and for dropping this check in the first place (honestly I do not remember why I dropped it, but I do remember that it was no accident ... I guess I was convinced that it would not do any harm ;)). chris On 11/21/2013 10:02 PM, Makarius wrote: On Thu, 21 Nov 2013, Dmitriy Traytel wrote: From my angle Isabelle/f6ffe53387ef resolves [1] in a robust way. But I'm waiting for Christian to confirm this. Chris, is this OK? I am ready to send f6ffe53387ef to the emergency release branch https://bitbucket.org/isabelle_project/isabelle-release Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2013-2 release
Sorry for the delay (I'm currently moving from Japan back to Austria, and moving in takes longer than expected... Thus only irregular internet access.) I'll have a look today in the afternoon if that is okay, otherwise I'm sure that Dmitriy knows what he is doing :-) cheers chris Makarius makar...@sketis.net wrote: On Thu, 21 Nov 2013, Dmitriy Traytel wrote: From my angle Isabelle/f6ffe53387ef resolves [1] in a robust way. But I'm waiting for Christian to confirm this. Chris, is this OK? I am ready to send f6ffe53387ef to the emergency release branch https://bitbucket.org/isabelle_project/isabelle-release Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle website
Maybe this thread is of interest http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03773.html (It contains an overview.html that I once started but never finished.) cheers chris On 09/30/2013 08:28 PM, Lawrence Paulson wrote: Early in 2013 I was planning to update the old PG-based movie to use jEdit, but was interrupted by massive programme committee obligations among other things, and it was left behind by events. And anyway jEdit has changed quite a bit since then. Perhaps I shall find the time after the next release. Probably not before. Larry On 30 Sep 2013, at 12:10, Makarius makar...@sketis.net wrote: This perspective can somehow be taken into account when updating the website. E.g. the old preview by Larry shows how to download, install, run Isabelle, open a theory file, but this is now self-explanatory. There could be some nice videos instead, but I still don't know how to produce them. ___ 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] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]
On 09/30/2013 07:33 PM, Makarius wrote: On Tue, 24 Sep 2013, Christian Sternagel wrote: After this changeset, variants may be arbitrary terms (due to localization). Now replacing a variant by the corresponding overloaded constant is done by rewriting (as Florian already pointed out, this happens in insert_overloaded) as follows fun insert_overloaded ctxt variant = (case try Term.type_of variant of NONE = variant | SOME T = Pattern.rewrite_term (Proof_Context.theory_of ctxt) [] [Option.map (Const o rpair T) o get_overloaded ctxt o Term.map_types (K dummyT)] variant); Apparently this interferes with abbreviations. Am I doing anything strange here? I've looked only briefly so far. Abbreviations are only contracted for type-correct terms, but above that information is not fully preserved. Pattern.rewrite_term needs to re-used the type of the replaced subterm (within the proc), not the overall type of the term called variant above. Thanks! That's a valuable hint. I will look into it and hope to make adhoc overloading and abbreviations produce the expected results again, before the release. cheers chris Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]
Thanks Jasmin! @Peter: Does this patch work with your developments as expected? cheers chris On 09/30/2013 10:18 PM, Jasmin Christian Blanchette wrote: Am 30.09.2013 um 15:07 schrieb Christian Sternagel c.sterna...@gmail.com: It seems that the required changes are minimal. See the attached patch. To be on the safe side: could somebody push this to the test server (in my local tests I just loaded all theories from the Isabelle repo and the AFP that contained the keyword adhoc_overloading in Isabelle/jEdit instead of building all heap images). Done. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [Fwd: [isabelle] Monad_Syntax breaks display of abbreviations]
Some more details: until 0d0c20a0a34f we have the expected behavior. With changeset: 52622:e0ff1625e96d user:wenzelm date:Fri Jul 12 16:19:05 2013 +0200 summary: localized and modernized adhoc-overloading (patch by Christian Sternagel); term bind (Some my_abbrev) f is not accepted at all (red, but no error message; but I think this is an orthogonal issue of implicit assumptions on my side that where not correct and which was resolved in the meanwhile). Nevertheless, this is the changeset I suspect to introduce the new behavior, since here the implementation of insert_internal_same (which is now called insert_overloaded) is drastically changed. Before this changeset variants are always Consts and thus replacing variants with their overloaded constant is easily done by pattern-matching on variants. After this changeset, variants may be arbitrary terms (due to localization). Now replacing a variant by the corresponding overloaded constant is done by rewriting (as Florian already pointed out, this happens in insert_overloaded) as follows fun insert_overloaded ctxt variant = (case try Term.type_of variant of NONE = variant | SOME T = Pattern.rewrite_term (Proof_Context.theory_of ctxt) [] [Option.map (Const o rpair T) o get_overloaded ctxt o Term.map_types (K dummyT)] variant); Apparently this interferes with abbreviations. Am I doing anything strange here? cheers chris On 09/24/2013 01:06 PM, Christian Sternagel wrote: Dear Florian and Peter, first, sorry for my long silence, I was on holidays. On 09/20/2013 12:30 AM, Florian Haftmann wrote: Hi Peter, hi Christian Referring to Isabelle_12-Sep-2013: When using overloading from Monad_Syntax, abbreviations are no longer displayed in output syntax: is this »no longer« referring to the state of Isabelle2013? Or did it also go wrong then? This works as expected with Isabelle2013. Most likely, my recent localization of adhoc overloading caused the new behavior (which I agree is not nice). I was not aware of this myself, thanks for bringing it to my attention. theory Scratch imports Main ~~/src/HOL/Library/Monad_Syntax abbreviation my_abbrev \equiv [True] term foo (Some my_abbrev) f (* Yields: foo (Some my_abbrev) f *) term bind (Some my_abbrev) f (* Yields: Some [True] = f*) A first analysis: theory Monad_Syn imports Main ~~/src/Tools/Adhoc_Overloading begin consts bind :: ['a, 'b ⇒ 'c] ⇒ 'd adhoc_overloading bind Set.bind Predicate.bind Option.bind List.bind abbreviation my_abbrev \equiv [True] term foo (Some my_abbrev) f (* Yields: foo (Some my_abbrev) f *) term bind (Some my_abbrev) f (* Yields: bind (Some [True]) f *) The monad syntax is not to blame, the problem is already in adhoc overloading. Using declare [[show_variants]] term foo (Some my_abbrev) f (* Yields: foo (Some my_abbrev) f *) term bind (Some my_abbrev) f (* Yields: Option.bind (Some my_abbrev) f *) Going to the corresponding lines in adhoc_overloading.ML: fun uncheck ctxt = if Config.get ctxt show_variants then I else map (insert_overloaded ctxt); I roughly guess something in insert_overloaded modifies the term in a way that the abbreviation does not apply any longer (again, only a rough guess). Thanks for the nice analysis. @Christian: maybe you have a suggestion what is going on here? At the moment not. I will investigate this issue and come back to the mailing list as soon as I find out more. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Find theorems and Sledgehammer Panels
My two cents, Last time I tried, there was no auto completion available in the input of the find theorem panel. Which makes the variant of typing find_theorems yourself in the main buffer more convenient for me at the moment. Also I experienced already several hangs with this panel as well as the sledgehammer panel. For the former that means that even after waiting for a long time nothing shows up, whereas for the latter the whole main buffer stays in a grayish highlighted state and does no longer produce output in response to edits (and also doesn't respond to clicking cancel). However, I cannot reliably reproduce either of that yet. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Improved completion mechanism
On 09/04/2013 02:24 AM, Makarius wrote: On Tue, 3 Sep 2013, Christian Sternagel wrote: Just for the record: the above mentioned hand also sometimes happens when typing V ... E ... R ... Y ... slowly ;). It is just more frequent when typing faster (mainly because a hang only ever happens directly after having pressed a key). OK, a few more hints what can be done right now. For practical use, you can try with the Isabelle/Scala option jedit_completion = false (via Plugin Options / Completion / Completion). This means there won't be any automatic popup or immdediate replacement anymore, just explicit C+b completion. Just to be sure, did you mean Plugins / Plugin Options / Isabelle / General / Completion / Completion? Furthermore, I still have Plugins / Plugin Options / Sidekick / General / Code Completion Options is that okay? cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Improved completion mechanism
On 09/04/2013 12:16 AM, Makarius wrote: In parallel to that, you can try a different Linux on your hardware, either just a virtual one, or one that is booted from a USB stick (Ubuntu supports that nicely). I did so with an 'Ubuntu 13.04 Raring Ringtail - Release amd64' live USB stick and was not able to reproduce the phenomenon, i.e., no hangs of the keyboard input. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL iff notation
Same here. - cheers chris Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: Are there clubs of iff vs. non-iff? If almost everybody is a member of the iff club we could just remove that print mode. (We don't have to consider that for the coming release, to avoid any real-time pressure on this question.) I am definitely a member of the iff-club. Partly for precedence reasons, but also because you can recognize predicate equations immediately. 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
Re: [isabelle-dev] NEWS: Improved completion mechanism
On 09/02/2013 06:30 PM, Makarius wrote: On Sat, 31 Aug 2013, Christian Sternagel wrote: First note that for me keyboard input to Isabelle/jEdit typically hangs every 10 minutes or so, depending on how fast I type (but this is an old and known issue). I was hoping that it would have disappeared altogether. So far the speculation was that the hang is due to the window manager and its built-in conflicts with JWindow etc. The popups are now done without separate window, as plain Swing JComponent. So the persisting hang indicates some problem in more elementary key hangling or plain text insertion into the text buffer. I have myself done a lot of empirical tests recently on several quite different systems, and I am also typing very fast, but did not see any problem like that. Just for the record: the above mentioned hand also sometimes happens when typing V ... E ... R ... Y ... slowly ;). It is just more frequent when typing faster (mainly because a hang only ever happens directly after having pressed a key). It looks like we need to make another round in the game of guessing at oddities that Fedora Linux might have installed. Yes please. How can I be of assistance (as apparently the only person having this kind of issue ;) ... maybe I should just buy a new computer, however, Fedora Linux is my preferred Platform, so maybe as soon as I get my hands on a different machine having Fedora installed -- which might take some time -- I should check whether this is specific to *my* laptop or a general issue of Fedora; or did we establish an answer already)? chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Improved completion mechanism
Dear Makarius, First note that for me keyboard input to Isabelle/jEdit typically hangs every 10 minutes or so, depending on how fast I type (but this is an old and known issue). In Isabelle2013 the completion popup was not triggered when deleting characters (with backspace). Now this is the case and it seems to cause more frequent hangs for me (since deleting is typically done very fast). Is this behavior intentional, and if yes, what is the gain? cheers chris On 08/30/2013 08:52 PM, Makarius wrote: * Improved completion mechanism, which is now managed by the Isabelle/jEdit plugin instead of SideKick. - Various Isabelle plugin options to control popup behaviour and immediate insertion into buffer. - Light-weight popup, which avoids explicit window (more reactive and more robust). Interpreted key events: TAB, ESCAPE, UP, DOWN, PAGE_UP, PAGE_DOWN. All other key events are passed to the jEdit text area unchanged. - Explicit completion via standard jEdit shortcut C+b, which has been remapped to action isabelle.complete (fall-back on regular complete-word for non-Isabelle buffers). - Implicit completion via keyboard input on text area, with popup or immediate insertion into buffer. - Implicit completion of plain words requires at least 3 characters (was 2 before). - Immediate completion ignores plain words; it requires 1 characters of symbol abbreviation to complete, otherwise fall-back on completion popup. - Isabelle Symbols are only completed in backslashed forms, e.g. \forall or \forall that both produce the Isabelle symbol \forall in its Unicode rendering. - Refined table of Isabelle symbol abbreviations (see $ISABELLE_HOME/etc/symbols). This refers to Isabelle/d0e4c8f73541. It is an intermediate somewhat stable stepping-stone -- it remains to be seen which of the other ideas on my list can be worked out before the release (it is getting quite close now). If there are any oddities in the new setup, or really bad things of the old one that are still there, please let me know about it. 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
[isabelle-dev] jEdit: re-checking of main buffer
Just an observation. Assuming that the grayish background highlighting really indicates prover activity in the background, I recently noticed that sometimes a re-check of the whole buffer is done in situations where this is (as far as I see) not necessary. For example, having lemma ... by auto lemma ... by auto when I select the second by auto (typically S+Home, since the courser is positioned directly behind it after just having typed it) and then replace the selected region by something different, the whole buffer is highlighted (thus re-chekced or re-parsed?). This is not the only such situation, but one that I could reproduce reliably. Note also that -- just making a subjective evaluation by feeling -- that this re-checking happens more frequently in a1cd4126a1c4 (and possibly earlier) than in Isabelle2013. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] functions over abstract data
Dear Alex and all,
once again I started to transform a rather adhoc parser datatype (in
IsaFoR) into some (I think) nicer variant using abstract datatypes with
invariants. After tinkering around for several days (where everything
worked out nicely) I hit a wall, and also remembered that I already did
so some years ago, when I wanted to do the same thing. Only this time,
instead of giving up, I started to think about destructing the wall (not
with my head though ... well ... in a way ;)).
Let me first state my problem (parsers are only a special instance).
Suppose you have an abstract datatype with invariant like
typedef T = {x. Inv x}
with an Abs/Rep pair and the invariant Inv.
-
*Example:* Parsers:
('a, 'b) raw_parser = 'a list = string + ('b * 'a list)
leq p - (ALL ts x ts'.
p ts = Inr (x, ts') -- length ts' = length ts)
typedef ('a, 'b) parser = {p::('a, 'b) raw_parser. leq p}
morphisms run Parser
-
When defining a function f, whose result type is T, it might be
necessary to peek under the hood in order to show termination. When
doing this manually, we destroy the abstraction and always have to
reason about the raw-level and even worse, also all the existing
constants with result type T have to be deconstructed in the definition.
-
*Example:* Suppose we already have do-notation for parsers
(i.e., bind), monadic return, op | (for alternatives),
and a parser just that parses just the given string. One
simple parser that could be constructed is:
par =
(do { just (, par; just ); return () }) |
return ()
However, without lifting the abstraction, we have no handle
on termination. Resulting in something like
par_aux ts = run
((do { just (, Parser par_aux; just ); return () }) |
return ())
ts
par = Parser par_aux
where I have to unfold all the abstract definitions in the
body of par_aux in order to prove termination and the
termination proof gets really messy (in fact I did not
succeed at all.)
-
Here comes my suggestion (until now I only did a manual --
i.e., all proofs and auxiliary definitions by hand --
case-study for the par parser, to check feasibility).
(This only makes sense when Rep returns something
of function type.)
Function specifications may be given parameters Abs, Rep,
Inv (most likely corresponding to some abstract datatype
with invariant) with lemmas:
Abs_inverse: Inv x == Rep (Abs x) = x
Rep_eqI: (!!x. Rep f x = Rep g x) == f = g
Then when the user writes something like
function (abstract Abs Rep Inv)
f :: T
where
f = F f
this is internally replaced by
Rep f x = Rep (F f) x
for the inductive definition of the function graph G_f, we replace the
existing (see Alex' thesis, page 17) introduction rules (for simplicity
just using a single recursive call):
(Gamma == (r[h/f], h(r[h/f]) : G_f) == (x, F h x) : G_f
by
(Gamma == (r[h/f], Rep h (r[h/f])) : G_f == (x, Rep (F h) x) : G_f
(So we more or less consider Rep f instead of just f to be the newly
defined function for the purpose of internal constructions.)
The introduction rules for the domain are modified similarly. The
internal definition of the function is now two-fold:
f' = (%x. THE y. par_graph x y)
f = Abs f'
Furthermore, an additional lemma (besides the usual x : dom_f == EX!y.
(x, y) : G_f) is needed:
Inv f' == x : dom_f == (x, Rep (F f) x) : G_f
(which is proved similarly to the existence part of the standard lemma
and where Inv f' is needed to obtain, together with Abs_inverse,
Rep f = f'.) Furthermore the usual psimps get an additional assumption:
psimps: Inv f' == x : dom_f == Rep f x = Rep (F f) x
Then the termination proof involves two steps:
- show !!x. x : dom_f, and
- show (!!x. x : dom_f) == inv f'
(which is both trivial for the par parser). Then we can derive Rep f
x = Rep (F f) x, which together with Rep_eqI yields the desired f =
F f.
Remark: ideally this should also handle additional parameters of f
(which are outside of the abstraction). Maybe something like:
f x = F f x
turned into
Rep (f x) y = Rep (F f x) y
with
f' = (%x y. THE z. ((x, y), z) : G_f
f = (%x. Abs (f' x))
Any comments? Would anybody else find this useful?
cheers
chris
PS: I started to dive into the function package. My first hurdle is that
for f not of function type (as in par), no recursive calls are
generated, since Function_Ctx_Tree.mk_tree says that No cong rules
could be found.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Monad_Syntax
Dear all,
any opinions on making the type of monadic bind more general (see the
attached patch)?
For my motivation see the farther below.
I tested the change against IsaFoR (which makes heavy use of
Monad_Syntax). Unfortunately, running JinjaThreads (which also uses
Monad_Syntax) timed out on my machine (hopefully not due to the patch).
Could anybody with access to a more powerful machine check this please?
Motivation:
I'm currently writing a small combinator parser library in Isabelle/HOL,
where (for reasons of totality) I have two types of parsers (both are
typedefs carved out from the function space 'a list = string + ('b *
'a list):
- standard parsers (with the invariant that the remaining input after
parsing is not longer than before), and
- consuming parsers (with the invariant that the remaining input
after parsing is strictly shorter than before).
Then it is possible to have (recursive) combinators like (where types
are simplified for readability)
many :: 'a cparser = ('a list) parser
where totality of many p relies on the fact that p consumes at least
one token. (Of course, it is trivial to turn a consuming parser into a
standard one.) Now for bind: let p, f be standard and cp and cf
be consuming. Then suitable combinations that yield consuming parsers are:
cp = cf, p = cf, and cp = f
But until now the type of Monad_Syntax.bind was 'a = ('b = 'c) =
'c which does not allow the last combination (since the result of f
is not consuming, but cp = f is).
Concerning readability it would be neat if I could overload bind for
all these cases.
Any comments?
cheers
chris
# HG changeset patch
# User Christian Sternagel
# Date 1376987651 -32400
# Tue Aug 20 17:34:11 2013 +0900
# Node ID 4808a6ae009b22369d71658c64369574d6adea83
# Parent 7e89edba3db64dad93dadac77a9e64d45ffcfe49
more general typing of monadic bind
diff --git a/src/HOL/Library/Monad_Syntax.thy b/src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy
+++ b/src/HOL/Library/Monad_Syntax.thy
@@ -15,7 +15,7 @@
*}
consts
- bind :: ['a, 'b \Rightarrow 'c] \Rightarrow 'c (infixr = 54)
+ bind :: ['a, 'b \Rightarrow 'c] \Rightarrow 'd (infixr = 54)
notation (xsymbols)
bind (infixr \guillemotright= 54)
@@ -24,7 +24,7 @@
bind (infixr \bind 54)
abbreviation (do_notation)
- bind_do :: ['a, 'b \Rightarrow 'c] \Rightarrow 'c
+ bind_do :: ['a, 'b \Rightarrow 'c] \Rightarrow 'd
where
bind_do \equiv bind
@@ -46,14 +46,14 @@
_do_then :: 'a \Rightarrow do_bind (_ [14] 13)
_do_final :: 'a \Rightarrow do_binds (_)
_do_cons :: [do_bind, do_binds] \Rightarrow do_binds (_;//_ [13, 12] 12)
- _thenM :: ['a, 'b] \Rightarrow 'b (infixr 54)
+ _thenM :: ['a, 'b] \Rightarrow 'c (infixr 54)
syntax (xsymbols)
_do_bind :: [pttrn, 'a] \Rightarrow do_bind ((_ \leftarrow/ _) 13)
- _thenM :: ['a, 'b] \Rightarrow 'b (infixr \guillemotright 54)
+ _thenM :: ['a, 'b] \Rightarrow 'c (infixr \guillemotright 54)
syntax (latex output)
- _thenM :: ['a, 'b] \Rightarrow 'b (infixr \then 54)
+ _thenM :: ['a, 'b] \Rightarrow 'c (infixr \then 54)
translations
_do_block (_do_cons (_do_then t) (_do_final e))
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] isabelle doc functions
Dear all,
I propose to apply the following patch to the documentation of the
function package. (I found two tiny typos which could have been
prevented by using @{thm [source] ...} -- which might not have existed
at the time of writing -- instead of @{text ...}, the patch (hopefully)
replaces all such references to theorem-names accordingly.)
cheers
chris
# HG changeset patch
# User Christian Sternagel
# Date 1376718288 -32400
# Sat Aug 17 14:44:48 2013 +0900
# Node ID be89d558ec26179cdd6da4629492ecca50c4829f
# Parent cba2ddfb30c47192ecfbb531494a423125a1bb8b
more document antiquotations (for proper theorem names);
diff --git a/src/Doc/Functions/Functions.thy b/src/Doc/Functions/Functions.thy
--- a/src/Doc/Functions/Functions.thy
+++ b/src/Doc/Functions/Functions.thy
@@ -87,7 +87,7 @@
Isabelle provides customized induction rules for recursive
functions. These rules follow the recursive structure of the
- definition. Here is the rule @{text sep.induct} arising from the
+ definition. Here is the rule @{thm [source] sep.induct} arising from the
above definition of @{const sep}:
@{thm [display] sep.induct}
@@ -387,7 +387,7 @@
text {*
When functions are mutually recursive, proving properties about them
- generally requires simultaneous induction. The induction rule @{text even_odd.induct}
+ generally requires simultaneous induction. The induction rule @{thm [source] even_odd.induct}
generated from the above definition reflects this.
Let us prove something about @{const even} and @{const odd}:
@@ -507,7 +507,7 @@
can be simplified to @{term F} with the original equations, a
(manual) case split on @{term x} is now necessary.
- \item The splitting also concerns the induction rule @{text
+ \item The splitting also concerns the induction rule @{thm [source]
And.induct}. Instead of five premises it now has seven, which
means that our induction proofs will have more cases.
@@ -730,11 +730,11 @@
text {*
\noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.psimps}\end{minipage}
- \hfill(@{text findzero.psimps})
+ \hfill(@{thm [source] findzero.psimps})
\vspace{1em}
\noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.pinduct}\end{minipage}
- \hfill(@{text findzero.pinduct})
+ \hfill(@{thm [source] findzero.pinduct})
*}
text {*
@@ -854,10 +854,10 @@
Since our function increases its argument at recursive calls, we
need an induction principle which works \qt{backwards}. We will use
- @{text inc_induct}, which allows to do induction from a fixed number
+ @{thm [source] inc_induct}, which allows to do induction from a fixed number
\qt{downwards}:
- \begin{center}@{thm inc_induct}\hfill(@{text inc_induct})\end{center}
+ \begin{center}@{thm inc_induct}\hfill(@{thm [source] inc_induct})\end{center}
Figure \ref{findzero_term} gives a detailed Isar proof of the fact
that @{text findzero} terminates if there is a zero which is greater
@@ -936,7 +936,7 @@
findzero_rel}, which was also created internally by the function
package. @{const findzero_rel} is just a normal
inductive predicate, so we can inspect its definition by
- looking at the introduction rules @{text findzero_rel.intros}.
+ looking at the introduction rules @{thm [source] findzero_rel.intros}.
In our case there is just a single rule:
@{thm[display] findzero_rel.intros}
@@ -955,9 +955,10 @@
Since the domain predicate is just an abbreviation, you can use
lemmas for @{const accp} and @{const findzero_rel} directly. Some
- lemmas which are occasionally useful are @{text accpI}, @{text
+ lemmas which are occasionally useful are @{thm [source] accpI}, @{thm [source]
accp_downward}, and of course the introduction and elimination rules
- for the recursion relation @{text findzero.intros} and @{text findzero.cases}.
+ for the recursion relation @{thm [source] findzero_rel.intros} and @{thm
+ [source] findzero_rel.cases}.
*}
section {* Nested recursion *}
@@ -1158,7 +1159,7 @@
congruence rule that specifies left-to-right evaluation order:
\vspace{1ex}
- \noindent @{thm disj_cong}\hfill(@{text disj_cong})
+ \noindent @{thm disj_cong}\hfill(@{thm [source] disj_cong})
\vspace{1ex}
Now the definition works without problems. Note how the termination
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] string and altstring
Dear all, currently it is possible to write something like \ , \\, `\``, or `\\` (i.e., there are escape sequences for the delimiters of strings and altstrings, as well as for backslash). What many people might be used to from programming languages does not work however, e.g., \n, \t, ... For that reason we currently have some abbreviations like the following in IsaFoR: abbreviation tab :: char where tab ≡ Char Nibble0 Nibble9 abbreviation newline :: char where newline ≡ Char Nibble0 NibbleA abbreviation carriage_return :: char where carriage_return ≡ Char Nibble0 NibbleD abbreviation wspace :: char list where wspace ≡ CHR '' '' # newline # tab # carriage_return # [] (Maybe there is a better solution?) Would it make sense to allow the most common escape sequences (like \n, \t, \r, etc.)? Then I could use CHR ''\t'', CHR ''\n'', CHR ''\r'', '' \n\t\r'' instead of the above. Btw: Why does CHR ''\013'' result in Char Nibble0 NibbleA? Shouldn't that be Char Nibble0 NibbleD? cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] partial_function
(Almost) everything back. I merely stumbled across a known issue (which
in hindsight I vaguely remember, but I did not find the corresponding
thread).
First I had to increase unify_search_bound (otherwise I obtained an
error as described in my previous email). What I did *not* notice
however, was the following message at the end of a very long trace (in
jEdit):
Tracing paused. Stop, or continue with next 100, 1000, 1 messages?
So, actually jEdit was just waiting for my input and not computing for
hours (as I thought; I should have observed that from the missing scream
of my laptops fan).
By setting unify_trace_bound to the same value for which
unify_search_bound succeeded, everything was fine again.
Sorry for the false alarm.
cheers
chris
On 08/06/2013 02:40 PM, Christian Sternagel wrote:
Dear all,
I'm currently checking IsaFoR [1] against the repository versions of
Isabelle (8d8cb75ab20a) and the AFP (05436df687d1). Doing so, I stumbled
across a partial_function definition that worked with Isabelle2013 but
aborts now with a Unification bound exceeded.
Is anybody aware of changes in partial_function or unification (or
somewhere I didn't think of) that could explain this?
The general shape of the function (which is employed to parse XML into
an internal datatype) is:
partial_function (parse_result)
...
where
parser x y = xml1element ''tag name'' (xml_options [
(''tag name 1'', parser_1),
(''tag name 2'', parser_2,
...
(''tag name N'', parser_N)
]) ...
where some of the parser_i use parser recursively. Currently we have
around 20 parsers in the above list and the error disappears if I reduce
that to 14 (with unify_search_bound = 90).
If anybody has the energy to look at the real code ;) see [2], theory
CPF_Parser.thy, partial function xml2dp_termination_proof. You will
also have to apply a patch from my local patch queue (which is
attached), since the official repository is for Isabelle2013.
cheers
chris
[1] http://cl-informatik.uibk.ac.at/software/ceta/
[2] http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] adhoc overloading
Dear Makarius,
actually even more is missing, since I was not able to properly use hg
export (I am used to hg bundle which exports *all* changesets that
are only local, whereas for hg export I have to give all revisions
that should be exported explicitly). Sorry for that. Please find
attached a file containing all my changes.
cheers
chris
On 08/06/2013 03:34 AM, Makarius wrote:
On Fri, 2 Aug 2013, Christian Sternagel wrote:
On 08/02/2013 12:04 AM, Makarius wrote:
On Wed, 17 Jul 2013, Christian Sternagel wrote:
in case anybody finds localized ad-hoc overloading useful.
Quite often it is just a matter to tell users about the existence of
such useful tools.
Do you feel like making an example theory, e.g.
src/HOL/ex/Adhoc_Overloading_Examples.thy or a short entry for the
isar-ref manual? E.g. somewhere here
http://isabelle.in.tum.de/repos/isabelle/annotate/122416054a9c/src/Doc/IsarRef/HOL_Specific.thy
I gave both a try. Please find the resulting changesets (via hg
export) attached (I also squeezed in some unrelated changes:
spell-checking, tuning of error messages. I hope that is okay).
The tuning etc. is fine (it looks like done with care).
What is missing in the commit is your new file
src/HOL/ex/Adhoc_Overloading_Examples.thy
Makarius
# HG changeset patch
# User Christian Sternagel
# Date 1375413062 -32400
# Fri Aug 02 12:11:02 2013 +0900
# Node ID 8173d8eb92c59711abede67ca2c035ed3e02beb6
# Parent cc425a7dc9adbcc95b7c6ed124466384e087275e
tuned formatting of error message
diff --git a/src/Tools/adhoc_overloading.ML b/src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML
+++ b/src/Tools/adhoc_overloading.ML
@@ -41,7 +41,7 @@
in term ::
quote (Syntax.string_of_term ctxt' t) ::
(if null instances then no instances else multiple instances:) ::
-map (Syntax.string_of_term ctxt') instances)
+map (Markup.markup Markup.item o Syntax.string_of_term ctxt') instances)
| error
end;
# HG changeset patch
# User Christian Sternagel
# Date 1375425679 -32400
# Fri Aug 02 15:41:19 2013 +0900
# Node ID f3ab98f28d70c18a919b23fbd6a5daffba212251
# Parent 8173d8eb92c59711abede67ca2c035ed3e02beb6
use uniform spelling of adhoc
diff --git a/src/Tools/Adhoc_Overloading.thy b/src/Tools/Adhoc_Overloading.thy
--- a/src/Tools/Adhoc_Overloading.thy
+++ b/src/Tools/Adhoc_Overloading.thy
@@ -2,7 +2,7 @@
Author: Christian Sternagel, University of Innsbruck
*)
-header {* Ad-hoc overloading of constants based on their types *}
+header {* Adhoc overloading of constants based on their types *}
theory Adhoc_Overloading
imports Pure
diff --git a/src/Tools/adhoc_overloading.ML b/src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML
+++ b/src/Tools/adhoc_overloading.ML
@@ -1,7 +1,7 @@
(* Author: Alexander Krauss, TU Muenchen
Author: Christian Sternagel, University of Innsbruck
-Ad-hoc overloading of constants based on their types.
+Adhoc overloading of constants based on their types.
*)
signature ADHOC_OVERLOADING =
@@ -227,12 +227,12 @@
val _ =
Outer_Syntax.local_theory @{command_spec adhoc_overloading}
-add ad-hoc overloading for constants / fixed variables
+add adhoc overloading for constants / fixed variables
(Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) adhoc_overloading_cmd true);
val _ =
Outer_Syntax.local_theory @{command_spec no_adhoc_overloading}
-add ad-hoc overloading for constants / fixed variables
+add adhoc overloading for constants / fixed variables
(Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) adhoc_overloading_cmd false);
end;
# HG changeset patch
# User Christian Sternagel
# Date 1375425721 -32400
# Fri Aug 02 15:42:01 2013 +0900
# Node ID 5e53d4373e38de46b1f0358aeca06ecd8fbb4bdb
# Parent f3ab98f28d70c18a919b23fbd6a5daffba212251
added examples of adhoc overloading
diff --git a/src/HOL/ex/Adhoc_Overloading_Examples.thy b/src/HOL/ex/Adhoc_Overloading_Examples.thy
new file mode 100644
--- /dev/null
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy
@@ -0,0 +1,250 @@
+(* Title: HOL/ex/Adhoc_Overloading_Examples.thy
+Author: Christian Sternagel
+*)
+
+header {* Ad Hoc Overloading *}
+
+theory Adhoc_Overloading_Examples
+imports
+ Main
+ ~~/src/Tools/Adhoc_Overloading
+ ~~/src/HOL/Library/Infinite_Set
+begin
+
+text {*Adhoc overloading allows to overload a constant depending on
+its type. Typically this involves to introduce an uninterpreted
+constant (used for input and output) and then add some variants (used
+internally).*}
+
+subsection {* Plain Ad Hoc Overloading *}
+
+text {*Consider the type of first-order terms.*}
+datatype ('a, 'b) term =
+ Var 'b |
+ Fun 'a ('a, 'b) term list
+
+text {*The set of variables of a term might be computed as follows.*}
+fun term_vars :: ('a, 'b) term \Rightarrow 'b set where
+ term_vars (Var x) = {x} |
+ term_vars (Fun f ts) = \Unionset (map term_vars ts)
+
+text {*However, also
Re: [isabelle-dev] adhoc overloading
On 08/02/2013 12:04 AM, Makarius wrote:
On Wed, 17 Jul 2013, Christian Sternagel wrote:
in case anybody finds localized ad-hoc overloading useful.
Quite often it is just a matter to tell users about the existence of
such useful tools.
Do you feel like making an example theory, e.g.
src/HOL/ex/Adhoc_Overloading_Examples.thy or a short entry for the
isar-ref manual? E.g. somewhere here
http://isabelle.in.tum.de/repos/isabelle/annotate/122416054a9c/src/Doc/IsarRef/HOL_Specific.thy
I gave both a try. Please find the resulting changesets (via hg
export) attached (I also squeezed in some unrelated changes:
spell-checking, tuning of error messages. I hope that is okay).
cheers
chris
# HG changeset patch
# User Christian Sternagel
# Date 1375425767 -32400
# Fri Aug 02 15:42:47 2013 +0900
# Node ID a854ff7d191ae0735664632516e3274a1e7bd2f7
# Parent 5e53d4373e38de46b1f0358aeca06ecd8fbb4bdb
some documentation for adhoc overloading;
spell-checked;
diff -r 5e53d4373e38 -r a854ff7d191a src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy Fri Aug 02 15:42:01 2013 +0900
+++ b/src/Doc/IsarRef/HOL_Specific.thy Fri Aug 02 15:42:47 2013 +0900
@@ -1,5 +1,5 @@
theory HOL_Specific
-imports Base Main ~~/src/HOL/Library/Old_Recdef
+imports Base Main ~~/src/HOL/Library/Old_Recdef ~~/src/Tools/Adhoc_Overloading
begin
chapter {* Higher-Order Logic *}
@@ -588,7 +588,7 @@
There are no fixed syntactic restrictions on the body of the
function, but the induced functional must be provably monotonic
- wrt.\ the underlying order. The monotonicitity proof is performed
+ wrt.\ the underlying order. The monotonicity proof is performed
internally, and the definition is rejected when it fails. The proof
can be influenced by declaring hints using the
@{attribute (HOL) partial_function_mono} attribute.
@@ -622,7 +622,7 @@
@{const partial_function_definitions} appropriately.
\item @{attribute (HOL) partial_function_mono} declares rules for
- use in the internal monononicity proofs of partial function
+ use in the internal monotonicity proofs of partial function
definitions.
\end{description}
@@ -1288,7 +1288,7 @@
morphisms} specification provides alternative names. @{command
(HOL) quotient_type} requires the user to prove that the relation
is an equivalence relation (predicate @{text equivp}), unless the
- user specifies explicitely @{text partial} in which case the
+ user specifies explicitly @{text partial} in which case the
obligation is @{text part_equivp}. A quotient defined with @{text
partial} is weaker in the sense that less things can be proved
automatically.
@@ -1318,7 +1318,7 @@
and @{method (HOL) descending} continues in the same way as
@{method (HOL) lifting} does. @{method (HOL) descending} tries
to solve the arising regularization, injection and cleaning
-subgoals with the analoguous method @{method (HOL)
+subgoals with the analogous method @{method (HOL)
descending_setup} which leaves the four unsolved subgoals.
\item @{method (HOL) partiality_descending} finds the regularized
@@ -1416,6 +1416,46 @@
problem, one should use @{command (HOL) ax_specification}.
*}
+section {* Adhoc overloading of constants *}
+
+text {*
+ \begin{tabular}{rcll}
+ @{command_def adhoc_overloading} : @{text local_theory \rightarrow local_theory} \\
+ @{command_def no_adhoc_overloading} : @{text local_theory \rightarrow local_theory} \\
+ @{attribute_def show_variants} : @{text attribute} default @{text false} \\
+ \end{tabular}
+
+ \medskip
+
+ Adhoc overloading allows to overload a constant depending on
+ its type. Typically this involves the introduction of an
+ uninterpreted constant (used for input and output) and the addition
+ of some variants (used internally). For examples see
+ @{file ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy} and
+ @{file ~~/src/HOL/Library/Monad_Syntax.thy}.
+
+ @{rail
+(@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
+(@{syntax nameref} (@{syntax term} + ) + @'and')
+ }
+
+ \begin{description}
+
+ \item @{command adhoc_overloading}~@{text c v\^isub1 ... v\^isubn}
+ associates variants with an existing constant.
+
+ \item @{command no_adhoc_overloading} is similar to
+ @{command adhoc_overloading}, but removes the specified variants
+ from the present context.
+
+ \item @{attribute show_variants} controls printing of variants
+ of overloaded constants. If enabled, the internally used variants
+ are printed instead of their respective overloaded constants. This
+ is occasionally useful to check whether the system agrees with a
+ user's expectations about derived variants.
+
+ \end{description}
+*}
chapter {* Proof tools *}
@@ -1553,7 +1593,7 @@
equations in the code generator. The option @{text no_code}
of the command @{command (HOL) setup_lifting} can turn off that
behavior and causes that code
Re: [isabelle-dev] adhoc overloading
Dear all,
please find attached patches for localizing
src/Tools/Adhoc_Overloading.thy. It should work like the previous
version in the non-local case, besides a more convenient interface,
i.e., instead of
setup {*
Adhoc_Overloading.add_overloaded @{const_name foo}
# Adhoc_Overloading.add_variant @{const_name foo} @{const_name bar}
*}
it is now
adhoc_overloading
foo bar
where bar may be an arbitrary term (not just a constant). For removing
ad-hoc overloading there is the command no_adhoc_overloading.
I tested the local case only on toy examples. Comments are welcome.
cheers
chris
On 07/11/2013 04:36 PM, Christian Sternagel wrote:
Dear all,
here is an update to my previous message. Corresponding patches are
attached (tested with `isabelle build_doc -pa` and `isabelle afp_build
-A`).
Some comments:
1) Variants are stored as terms but where all types are mapped to
dummyT (which makes it easier to check for a given term, whether it is
a variant of an overloaded constant).
2) In the table that maps overloaded constants to variants in addition
to the dummy-typed variant also a type is included (where all free
type variables are replaced by schematic ones).
3) As stated by Dmitriy in the type unification thread the current
solution does not work for localization (but the corresponding change is
trivial, I'm just avoiding it for the moment, since without localization
I have to work with a thy, which is inconvenient to turn into a ctxt as
required by Variable.polymorphic).
cheers
chris
On 07/10/2013 04:38 PM, Christian Sternagel wrote:
First of all, thanks for all the useful answers and sorry for my late
reply (I visited a conference and had some holidays ;)). As Alexander
suggested, I first tried to modify the existing adhoc_overloading.ML in
such a way that variants may be arbitrary terms. Please find the results
of my attempt attached (the new adhoc_overloading.ML as well as a
patch-file). Now I will investigate further localization.
Any comments are welcome.
cheers
chris
On 06/02/2013 08:55 AM, Alexander Krauss wrote:
Hi Chris,
I'm currently (as of changeset e6433b34364b) investigating whether it
would be possible to allow adhoc overloading (implemented in
~~/src/Tools/adhoc_overloading.ML) inside local contexts.
Nice!
For completeness find my current adhoc_overloading.ML attached
Apart from the various formalities pointed out by Makarius, here is
another concern, which relates to Florian's earlier question about how
local you want to be...
Currently, Adhoc_Overloading replaces constants with other constants,
which makes it global-only. Your current version tries to deal with
Frees similarly, it's not just that. Recall the example you gave
previously:
consts FOO :: ... (some syntax)
setup {* Adhoc_Overloading.add_overloaded @{const_name FOO} *}
locale foo =
fixes foo :: ...
assumes ...
begin
local_setup {*
Adhoc_Overloading.add_variant @{const_name FOO} @{term foo}
*}
Now consider the following interpretation:
interpretation foo some term
proof
Now, some term should become a variant of FOO, so at least the variant
side of the overloading relation must be an arbitrary term. With your
current code, the overloading would only survive interpretations where
foo happens to be mapped to a constant.
So, I guess that the overloaded constants should remain constants, since
they are just syntactic anyway. It seems that localizing those would be
rather artificial. But the variants must be properly localized and
subject to the morphism.
As a step towards proper localization, you could start with the global
code, and first generalize it to accept arbitrary terms as variants.
Note that this touches in particular the uncheck phase, which can no
longer use Term_Subst.map_aterms_same (or Term.map_aterms), since it
becomes general rewriting. One must resort to the more general
Pattern.rewrite_term here. When all this is working again, the actual
localization is then a mere formality, of which you have already
discovered the ingredients.
Makarius wrote:
* Same.function seems to be a let-over from the version by Alex
Krauss. He had that once in his function package, copied from
somewhere else (probably old code of mine).
No, it has nothing to do with the function package, which never used any
Same stuff. It just arose rather naturally from the requirement to
return NONE when nothing changes... So it was not meant as an
optimization.
There is no point to do
such low-level optimizations in the syntax layer. It is for hardcore
kernel operations only
So should I manually check the result for equality, or does the
framework do this for me?
Alex
diff -r 908304753f7d thys/JinjaThreads/Framework/FWState.thy
--- a/thys/JinjaThreads/Framework/FWState.thy Thu Jul 11 13:37:41 2013 +0200
+++ b/thys/JinjaThreads/Framework/FWState.thy Fri Jul 12 19:47:05 2013 +0900
@@ -188,15 +188,9 @@
_ta_lock la l == CONST
Re: [isabelle-dev] adhoc overloading
The patches should be ready to push (for your convenience I attached
them once more; the attached patches are the same as from my previous
e-mail). Btw, I generated the patches against Isabelle 8afb396d9178 and
AFP 908304753f7d (but I guess this information is also included in the
patches ;)).
cheers
chris
On 07/12/2013 08:38 PM, Makarius wrote:
On Fri, 12 Jul 2013, Makarius wrote:
On Fri, 12 Jul 2013, Christian Sternagel wrote:
Dear all,
please find attached patches for localizing
src/Tools/Adhoc_Overloading.thy.
I will take care to apply the changesets to Isabelle and AFP.
Looking closer, I see several versions of patches. Are you still
exploring, or ready for push? Which version?
Makarius
diff -r 8afb396d9178 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jul 11 21:34:50 2013 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Jul 12 19:19:43 2013 +0900
@@ -274,10 +274,8 @@
Some (x, h') \Rightarrow execute (g x) h'
| None \Rightarrow None)
-setup {*
- Adhoc_Overloading.add_variant
-@{const_name Monad_Syntax.bind} @{const_name Heap_Monad.bind}
-*}
+adhoc_overloading
+ Monad_Syntax.bind Heap_Monad.bind
lemma execute_bind [execute_simps]:
execute f h = Some (x, h') \Longrightarrow execute (f \guillemotright= g) h = execute (g x) h'
diff -r 8afb396d9178 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy Thu Jul 11 21:34:50 2013 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy Fri Jul 12 19:19:43 2013 +0900
@@ -69,12 +69,7 @@
_do_block (_do_final e) = e
(m n) = (m = (\lambda_. n))
-setup {*
- Adhoc_Overloading.add_overloaded @{const_name bind}
- # Adhoc_Overloading.add_variant @{const_name bind} @{const_name Set.bind}
- # Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
- # Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
- # Adhoc_Overloading.add_variant @{const_name bind} @{const_name List.bind}
-*}
+adhoc_overloading
+ bind Set.bind Predicate.bind Option.bind List.bind
end
diff -r 8afb396d9178 src/Tools/Adhoc_Overloading.thy
--- a/src/Tools/Adhoc_Overloading.thy Thu Jul 11 21:34:50 2013 +0200
+++ b/src/Tools/Adhoc_Overloading.thy Fri Jul 12 19:19:43 2013 +0900
@@ -6,10 +6,10 @@
theory Adhoc_Overloading
imports Pure
+keywords adhoc_overloading :: thy_decl and no_adhoc_overloading :: thy_decl
begin
ML_file adhoc_overloading.ML
-setup Adhoc_Overloading.setup
end
diff -r 8afb396d9178 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML Thu Jul 11 21:34:50 2013 +0200
+++ b/src/Tools/adhoc_overloading.ML Fri Jul 12 19:19:43 2013 +0900
@@ -6,11 +6,14 @@
signature ADHOC_OVERLOADING =
sig
- val add_overloaded: string - theory - theory
- val add_variant: string - string - theory - theory
-
+ val is_overloaded: Proof.context - string - bool
+ val generic_add_overloaded: string - Context.generic - Context.generic
+ val generic_remove_overloaded: string - Context.generic - Context.generic
+ val generic_add_variant: string - term - Context.generic - Context.generic
+ (*If the list of variants is empty at the end of generic_remove_variant, then
+ generic_remove_overloaded is called implicitly.*)
+ val generic_remove_variant: string - term - Context.generic - Context.generic
val show_variants: bool Config.T
- val setup: theory - theory
end
structure Adhoc_Overloading: ADHOC_OVERLOADING =
@@ -18,122 +21,208 @@
val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false);
-
(* errors *)
-fun duplicate_variant_err int_name ext_name =
- error (Constant ^ quote int_name ^ is already a variant of ^ quote ext_name);
+fun duplicate_variant_error oconst =
+ error (Duplicate variant of ^ quote oconst);
-fun not_overloaded_err name =
- error (Constant ^ quote name ^ is not declared as overloaded);
+fun not_a_variant_error oconst =
+ error (Not a variant of ^ quote oconst);
-fun already_overloaded_err name =
- error (Constant ^ quote name ^ is already declared as overloaded);
+fun not_overloaded_error oconst =
+ error (Constant ^ quote oconst ^ is not declared as overloaded);
-fun unresolved_err ctxt (c, T) t reason =
- error (Unresolved overloading of ^ quote c ^ :: ^
+fun unresolved_overloading_error ctxt (c, T) t reason =
+ error (Unresolved overloading of ^ quote c ^ :: ^
quote (Syntax.string_of_typ ctxt T) ^ in ^
quote (Syntax.string_of_term ctxt t) ^ ( ^ reason ^ ));
+(* generic data *)
-(* theory data *)
+fun variants_eq ((v1, T1), (v2, T2)) =
+ Term.aconv_untyped (v1, v2) andalso T1 = T2;
-structure Overload_Data = Theory_Data
+structure Overload_Data = Generic_Data
(
type T =
-{ internalize : (string * typ) list Symtab.table,
- externalize : string Symtab.table };
- val empty = {internalize=Symtab.empty, externalize=Symtab.empty};
+{variants : (term * typ) list
Re: [isabelle-dev] type unification
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
You are right. Thanks for the clarification! - chris
On 07/11/2013 04:19 PM, Dmitriy Traytel wrote:
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] adhoc overloading
Dear all,
here is an update to my previous message. Corresponding patches are
attached (tested with `isabelle build_doc -pa` and `isabelle afp_build -A`).
Some comments:
1) Variants are stored as terms but where all types are mapped to
dummyT (which makes it easier to check for a given term, whether it is
a variant of an overloaded constant).
2) In the table that maps overloaded constants to variants in addition
to the dummy-typed variant also a type is included (where all free
type variables are replaced by schematic ones).
3) As stated by Dmitriy in the type unification thread the current
solution does not work for localization (but the corresponding change is
trivial, I'm just avoiding it for the moment, since without localization
I have to work with a thy, which is inconvenient to turn into a ctxt as
required by Variable.polymorphic).
cheers
chris
On 07/10/2013 04:38 PM, Christian Sternagel wrote:
First of all, thanks for all the useful answers and sorry for my late
reply (I visited a conference and had some holidays ;)). As Alexander
suggested, I first tried to modify the existing adhoc_overloading.ML in
such a way that variants may be arbitrary terms. Please find the results
of my attempt attached (the new adhoc_overloading.ML as well as a
patch-file). Now I will investigate further localization.
Any comments are welcome.
cheers
chris
On 06/02/2013 08:55 AM, Alexander Krauss wrote:
Hi Chris,
I'm currently (as of changeset e6433b34364b) investigating whether it
would be possible to allow adhoc overloading (implemented in
~~/src/Tools/adhoc_overloading.ML) inside local contexts.
Nice!
For completeness find my current adhoc_overloading.ML attached
Apart from the various formalities pointed out by Makarius, here is
another concern, which relates to Florian's earlier question about how
local you want to be...
Currently, Adhoc_Overloading replaces constants with other constants,
which makes it global-only. Your current version tries to deal with
Frees similarly, it's not just that. Recall the example you gave
previously:
consts FOO :: ... (some syntax)
setup {* Adhoc_Overloading.add_overloaded @{const_name FOO} *}
locale foo =
fixes foo :: ...
assumes ...
begin
local_setup {*
Adhoc_Overloading.add_variant @{const_name FOO} @{term foo}
*}
Now consider the following interpretation:
interpretation foo some term
proof
Now, some term should become a variant of FOO, so at least the variant
side of the overloading relation must be an arbitrary term. With your
current code, the overloading would only survive interpretations where
foo happens to be mapped to a constant.
So, I guess that the overloaded constants should remain constants, since
they are just syntactic anyway. It seems that localizing those would be
rather artificial. But the variants must be properly localized and
subject to the morphism.
As a step towards proper localization, you could start with the global
code, and first generalize it to accept arbitrary terms as variants.
Note that this touches in particular the uncheck phase, which can no
longer use Term_Subst.map_aterms_same (or Term.map_aterms), since it
becomes general rewriting. One must resort to the more general
Pattern.rewrite_term here. When all this is working again, the actual
localization is then a mere formality, of which you have already
discovered the ingredients.
Makarius wrote:
* Same.function seems to be a let-over from the version by Alex
Krauss. He had that once in his function package, copied from
somewhere else (probably old code of mine).
No, it has nothing to do with the function package, which never used any
Same stuff. It just arose rather naturally from the requirement to
return NONE when nothing changes... So it was not meant as an
optimization.
There is no point to do
such low-level optimizations in the syntax layer. It is for hardcore
kernel operations only
So should I manually check the result for equality, or does the
framework do this for me?
Alex
diff -r aaec3f5a1ba6 thys/JinjaThreads/Framework/FWState.thy
--- a/thys/JinjaThreads/Framework/FWState.thy Wed Jul 10 15:19:23 2013 +0200
+++ b/thys/JinjaThreads/Framework/FWState.thy Thu Jul 11 16:30:08 2013 +0900
@@ -190,12 +190,12 @@
setup {*
Adhoc_Overloading.add_overloaded @{const_name inject_thread_action}
- # Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name NewThreadAction}
- # Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name ConditionalAction}
- # Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name WaitSetAction}
- # Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name InterruptAction}
- # Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name ObsAction}
- # Adhoc_Overloading.add_variant @{const_name inject_thread_action} @{const_name LockAction
Re: [isabelle-dev] adhoc overloading
First of all, thanks for all the useful answers and sorry for my late
reply (I visited a conference and had some holidays ;)). As Alexander
suggested, I first tried to modify the existing adhoc_overloading.ML in
such a way that variants may be arbitrary terms. Please find the results
of my attempt attached (the new adhoc_overloading.ML as well as a
patch-file). Now I will investigate further localization.
Any comments are welcome.
cheers
chris
On 06/02/2013 08:55 AM, Alexander Krauss wrote:
Hi Chris,
I'm currently (as of changeset e6433b34364b) investigating whether it
would be possible to allow adhoc overloading (implemented in
~~/src/Tools/adhoc_overloading.ML) inside local contexts.
Nice!
For completeness find my current adhoc_overloading.ML attached
Apart from the various formalities pointed out by Makarius, here is
another concern, which relates to Florian's earlier question about how
local you want to be...
Currently, Adhoc_Overloading replaces constants with other constants,
which makes it global-only. Your current version tries to deal with
Frees similarly, it's not just that. Recall the example you gave
previously:
consts FOO :: ... (some syntax)
setup {* Adhoc_Overloading.add_overloaded @{const_name FOO} *}
locale foo =
fixes foo :: ...
assumes ...
begin
local_setup {*
Adhoc_Overloading.add_variant @{const_name FOO} @{term foo}
*}
Now consider the following interpretation:
interpretation foo some term
proof
Now, some term should become a variant of FOO, so at least the variant
side of the overloading relation must be an arbitrary term. With your
current code, the overloading would only survive interpretations where
foo happens to be mapped to a constant.
So, I guess that the overloaded constants should remain constants, since
they are just syntactic anyway. It seems that localizing those would be
rather artificial. But the variants must be properly localized and
subject to the morphism.
As a step towards proper localization, you could start with the global
code, and first generalize it to accept arbitrary terms as variants.
Note that this touches in particular the uncheck phase, which can no
longer use Term_Subst.map_aterms_same (or Term.map_aterms), since it
becomes general rewriting. One must resort to the more general
Pattern.rewrite_term here. When all this is working again, the actual
localization is then a mere formality, of which you have already
discovered the ingredients.
Makarius wrote:
* Same.function seems to be a let-over from the version by Alex
Krauss. He had that once in his function package, copied from
somewhere else (probably old code of mine).
No, it has nothing to do with the function package, which never used any
Same stuff. It just arose rather naturally from the requirement to
return NONE when nothing changes... So it was not meant as an optimization.
There is no point to do
such low-level optimizations in the syntax layer. It is for hardcore
kernel operations only
So should I manually check the result for equality, or does the
framework do this for me?
Alex
(* Author: Alexander Krauss, TU Muenchen
Author: Christian Sternagel, University of Innsbruck
Ad-hoc overloading of constants based on their types.
*)
signature ADHOC_OVERLOADING =
sig
val add_overloaded: string - theory - theory
val add_variant: string - term - theory - theory
val show_variants: bool Config.T
val setup: theory - theory
end
structure Adhoc_Overloading: ADHOC_OVERLOADING =
struct
val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false);
(* errors *)
fun duplicate_variant_error ext_name =
error (Duplicate variant of ^ quote ext_name);
fun not_overloaded_error name =
error (Constant ^ quote name ^ is not declared as overloaded);
fun already_overloaded_error name =
error (Constant ^ quote name ^ is already declared as overloaded);
fun unresolved_overloading_error ctxt (c, T) t reason =
error (Unresolved overloading of ^ quote c ^ :: ^
quote (Syntax.string_of_typ ctxt T) ^ in ^
quote (Syntax.string_of_term ctxt t) ^ ( ^ reason ^ ));
(* theory data *)
structure Overload_Data = Theory_Data
(
type T =
{internalize : term list Symtab.table,
externalize : string Termtab.table};
val empty = {internalize = Symtab.empty, externalize = Termtab.empty};
val extend = I;
fun merge_ext _ (ext_name1, ext_name2) =
if ext_name1 = ext_name2 then ext_name1
else duplicate_variant_error ext_name1;
fun merge
({internalize = int1, externalize = ext1},
{internalize = int2, externalize = ext2}) : T =
{internalize = Symtab.merge_list (op aconv) (int1, int2),
externalize = Termtab.join merge_ext (ext1, ext2)};
);
fun map_tables f g =
Overload_Data.map (fn {internalize = int, externalize = ext} =
{internalize = f int, externalize = g ext});
val is_overloaded = Symtab.defined o #internalize o Overload_Data.get;
val
[isabelle-dev] type unification
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] enumerating infinite sets of well-ordered elements
Dear all, I find myself considering the following cases every now and then: 1) If we know that some property P is true for infinitely many elements of a well-ordered set (all my use-cases so far, just concern natural numbers) it is in principle trivial to enumerate them in increasing order. Thus it should also be trivial to do so in Isabelle. 2) For a well-ordered set of elements and a fixed element N, assume that for every i = N there is a j i, s.t., the predicate P i j holds. Thus it is in principle trivial to construct a chain f, s.t., for all i, we have P (f i) (f (Suc i)) and f i f (Suc i). Again this should be trivial in Isabelle. Why not add corresponding functions and lemmas to the library? Please find attached a theory that handles these cases. The names of the locales are not ideal (please provide better ones ;)). Note that the first locale infinitely_many1 is a generalization of infinitely_many from theory Seq of the AFP entry Abstract-Rewriting. Currently the attached theory is part of AFP/Well-Quasi-Orders. cheers chris Least_Enum.thy Description: application/example ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP sitegen
Thanks for the quick answers. In case I'm not supposed to run tool/sitegen myself, just let me know ;) cheers chris On 06/06/2013 03:54 PM, Andreas Lochbihler wrote: Sorry for the confusion, I never ran sitegen.py myself because I thought that to be the priviledge of the editors. As Gerwin has found out, I dropped these links manually in 376347e6131a because they all were broken after the update on sourceforge. I decided not to update them for three reasons: 1. Most other entries do not link to changeset revisions; Category is now the only exception. Often they don't even mention the revision ID at all. 2. It is unclear when the links will break again if they are not checked automatically. 3. On the entry page, the links are visually the most prominent part of the change history, although they are the least relevant bit of information in the change history. If sitegen.py automatically links to the changesets, I'd be happy. But then, I suggest that the links are not formatted as highlighted as they are now. Andreas On 06/06/13 08:09, Gerwin Klein wrote: It looks like Andreas dropped these manually for his entries, so nothing really went wrong with the tools, he was just reacting to the sourceforge update leading to broken links. The URL scheme for linking to revision IDs in the new sourceforge setup is http://sourceforge.net/p/afp/code/ci/change-set-hash The short hashes that we normally use seem to work fine (it shows you long ones by default when you browse). It's up to the authors to have change set ids as links or not, so I'm not adding them back in myself. If Andreas is reading this and prefers having them in, by all means put them back. We haven't really made up our minds if developers should run admin/sitegen after updating history in metadata. I'd say, if you feel comfortable using sitegen and check that your changes are confined to history (as Chris apparently did), this is Ok to do. If you're not feeling comfortable doing this yourself, you change will just show up on the devel website the next time someone runs sitegen. We could try make sitegen.py aware of hg revision ids and make it link them automatically. If there's a volunteer for implementing this, I'm happy to consider this. Cheers, Gerwin On 06.06.2013, at 1:52 PM, Gerwin Klein gerwin.kl...@nicta.com.au wrote: I'll have a look at it. The links shouldn't be dropped, something is going wrong there. Cheers, Gerwin On 06/06/2013, at 1:48 PM, Christian Sternagel c.sterna...@gmail.com wrote: Btw: the links do not seem to work anyway. But why not replace them with working links instead of just dropping them? On 06/06/2013 12:40 PM, Christian Sternagel wrote: Dear all, to update the change history of one of my AFP entries, I ran admin/sitegen. I noticed that as a result some other sites changed too. All the changes where along the lines of -(revision a href=http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/f74a8be156a7;f74a8be156a7/a)br +(revision f74a8be156a7)br in corresponding *.shtml files, i.e., links to changesets are replaced by the mere short-form changeset ID. Is this on purpose or did I do something wrong? (I will of course refrain from pushing any changes until I got an answer.) cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] AFP sitegen
Dear all, to update the change history of one of my AFP entries, I ran admin/sitegen. I noticed that as a result some other sites changed too. All the changes where along the lines of -(revision a href=http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/f74a8be156a7;f74a8be156a7/a)br +(revision f74a8be156a7)br in corresponding *.shtml files, i.e., links to changesets are replaced by the mere short-form changeset ID. Is this on purpose or did I do something wrong? (I will of course refrain from pushing any changes until I got an answer.) cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP sitegen
Btw: the links do not seem to work anyway. But why not replace them with working links instead of just dropping them? On 06/06/2013 12:40 PM, Christian Sternagel wrote: Dear all, to update the change history of one of my AFP entries, I ran admin/sitegen. I noticed that as a result some other sites changed too. All the changes where along the lines of -(revision a href=http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/f74a8be156a7;f74a8be156a7/a)br +(revision f74a8be156a7)br in corresponding *.shtml files, i.e., links to changesets are replaced by the mere short-form changeset ID. Is this on purpose or did I do something wrong? (I will of course refrain from pushing any changes until I got an answer.) cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] adhoc overloading
Dear all,
as I said earlier I am trying to make some changes (in Generic_Data)
persistent from inside a command. (My special case is ad-hoc
overloading, but I think that is irrelevant for the following.)
My current setup is (could you please point out any inadequate choices):
- To set up a command (adhoc_overloading in my case) that should also
work inside local contexts I use Outer_Syntax.local_theory.
- For data related to the command I use Generic_Data (since it should
be available in top-level theories as well as local contexts).
- Investigating notation a bit (but not understanding the
implementation details ;)), I suspect that Local_Theory.declaration is
used to make changes in my Generic_Data persistent. What is the
purpose of the {syntax: bool, pervasive: bool} argument of
Local_Theory.declaration.
- Local_Theory.declaration expects a declaration as argument, which
abbreviates the type morphism - Context.generic - Context.generic.
For the time being I just ignore morphism (of course I will have to
understand and incorporate it at some point). So my declaration is
essentially a call to Context.mapping which takes two mappings: f
for theory - theory and g for Proof.context - Proof.context.
- So far so good. Everything compiles fine. When I actually use my newly
defined command, I get the error Stale theory encountered. So
obviously I'm doing something wrong in the above f (if I replace f
by I the error disappears, but of course then I can also not make
changes in my Generic_Data persistent.)
- Even if f is replaced by I above, something I do not understand
happens w.r.t. g. But this is specific to my adhoc_overloading so I
have to give some more details:
adhoc_overloading
foo foo_list
parses foo and foo_list with Parse.const and preprocesses all its
arguments by Proof_Context.read_const ctxt false dummyT, which I
thought was the canonical way to check whether a string is a (locally
fixed) constant.
Now inside a local context
context
fixes foo_nat :: nat
begin
I try
adhoc_overloading
foo foo_nat
And obtain
Unknown constant: foo_nat
When adding some debug output to my internal function I obtain the
following before the error:
checking constant: foo
const
DONE.
checking constant: foo_nat
free
DONE.
checking constant: foo
const
DONE.
checking constant: foo_nat
Unknown constant: foo_nat
Which tells me that once foo_nat is parsed as a locally fixed constant
(represented by a Free variable) as expected. What I did not expect was
that all the arguments are considered a second time (so actually g is
called twice). In this second run we are apparently in a different
context, since foo_nat is no longer locally fixed. I'm sure that this
is the correct behavior, but maybe someone could explain it to me.
For completeness find my current adhoc_overloading.ML attached (but be
aware that it is far from finished; it is merely a sandbox in which I
play to find out more about the internals of Isabelle).
Sorry for the lengthy email, but it's really hard to find your way
through the existing Isabelle/ML API without professional help ;)
cheers
chris
On 05/31/2013 06:08 AM, Makarius wrote:
On Wed, 29 May 2013, Florian Haftmann wrote:
Alternatively, use Context. directly in the body of the ML file
(which, I guess, is nowadays preferred over explicit setup in the
surrounding theory).
Hypersearch over the sources shows that Context. is still quite rare,
and there is no trend to be seen yet. Of course, a trend could be
started now.
Last time we've discussed that privately, you were more in favour of
setup and I more in favour of Context. (quite some years ago).
I am myself used to Context. in Isabelle/Pure (there is no other way),
and I follow the old habit with 'setup' in Isabelle/HOL most of the time.
On the other hand, the received two-part idiom is a bit odd wrt. proper
modularity:
ML_file foo.ML
setup Foo.setup
Like two-component glue to be fit together by hand. It used to be three
components until recently, with extra uses in the theory header.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
(* Author: Alexander Krauss, TU Muenchen
Author: Christian Sternagel, University of Innsbruck
Ad-hoc overloading of constants based on their types.
*)
signature ADHOC_OVERLOADING =
sig
val is_overloaded: Context.generic - string - bool
val overload: bool - string - Context.generic - Context.generic
val variant: bool - string - (string * typ) - Context.generic -
Context.generic
val show_overloaded: bool Config.T
end
structure Adhoc_Overloading: ADHOC_OVERLOADING =
struct
val show_overloaded = Attrib.setup_config_bool @{binding show_overloaded} (K
true);
(* errors *)
fun already_overloaded_error oconst =
error (Constant ^ quote oconst ^ is already
Re: [isabelle-dev] auto raises a TYPE exception
Hopefully it is all a bit more precise now. Maybe someone wants to formalize pattern.ML + unify.ML after 20 years, to pin down the remaining uncertaincies about type instantiation within these non-trivial algorithms. Just for the record, I would be interested in joining such an endeavor. Unfortunately I'm not a proven expert ;) cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle/jEdit - code completion
Dear all, I think a similar mail was sent a while ago (but I do not remember by whom and also was unable to excavate it): 1) In code completion the order of suggestions is sometimes odd (meaning that a different order would make the usual work-flow smoother). E.g., when I start with find I usually want find_theorems, but since find_consts is first in the list I have to type up to find_t (or use the arrow keys, which is even worse). Would it make sense to prioritize the suggestions (in a way a user can modify according to personal preference)? 2) Other code completion suggestions are just too short to make sense at all, e.g., when starting with fo suggesting for seems odd. In my opinion, since you need to type at least 2 characters to trigger code completion, suggestions that only have 3 letters should not be given, since they do not save anything. 3) Another nice thing would be to make code completion context sensitive (typically inside quotes you want to get different suggestions than at the top-level). I'm not saying that those are important issues, just trivial observations. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP access confusion
Dear Florian, I just confirmed that I get the same error message for my default afp-devel clone (i.e., it used to work with afp.hg.sourceforge.net/hgroot/afp/afp). cheers chris On 03/23/2013 07:01 PM, Florian Haftmann wrote: cf. doc/maintenance.html: Check out the archive from the mercurial repository with: hg clone ssh://login@afp.hg.sourceforge.net/hgroot/afp/afp afp-devel But hg pull ssh://fhaftm...@afp.hg.sourceforge.net/hgroot/afp/afp yields Remote: abort: There is no Mercurial repository here (.hg not found)! I'm stymied… Thanks for any hint, 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] Zorn's lemma, the well-ordering-theorem, and extending well-founded relations to (total) well-orders
On 02/28/2013 11:46 PM, Andrei Popescu wrote: Hi Christian, I am back from a 3-day trip which prevented me from answering sooner. Many thanks for your contribution! I'll go ahead and integrate your new Isar proofs of existing theorems and your new theorems. But, same as Larry, I do now quite understand why do you want to split Zorn and avoid certain dependencies. Maybe I confused myself ;). If I remember correctly, I can only build the bitbucket repo, if I have the separate Ordinal_Sum, since Constructions_on_Wellorders contains a reference to well_order_on from the old Zorn. Thus it seems that for this case the dependencies have to change (such that we can use the ordinal sum in Well_Order_Embedding). Ah, but I just see that you only wondered about the split of Zorn ... Well, never mind. Let's just forget about the split ;) (I guess it is just personal taste that I prefer more smaller theories over fewer bigger ones). Btw: The new name order-extension principle was nonsense, sorry (I backed this change out again). This is usually used to extend partial orders to total orders but says nothing about well-foundedness... does anybody have a better name, or should we stick to Well_Order_Extension? cheers chris Andrei --- On *Thu, 2/28/13, Lawrence Paulson /l...@cam.ac.uk/* wrote: From: Lawrence Paulson l...@cam.ac.uk Subject: Re: [isabelle-dev] Zorn's lemma, the well-ordering-theorem, and extending well-founded relations to (total) well-orders To: Christian Sternagel c.sterna...@gmail.com Cc: isabelle-dev isabelle-dev@mailbroy.informatik.tu-muenchen.de, Andrei Popescu uuo...@yahoo.com Date: Thursday, February 28, 2013, 4:04 PM I'm all in favour of refactoring the proofs. That might occasion moving material from one file to another. But I would keep that to a minimum. It isn't unusual to go deep into the past when investigating the origins of some issue. Larry On 27 Feb 2013, at 12:14, Christian Sternagel c.sterna...@gmail.com /mc/compose?to=c.sterna...@gmail.com wrote: Dear Larry please note that my proposal is not just about a split of the existing theory Zorn.thy, but also about a modernization of part of it (which I think makes it easier to understand, but I might be wrong... could be that the main purpose of this experiment was just to make me understand the formalized proofs ;)) as well as adding new facts (the order-extension principle). So please consider it, even if no split is done. Nevertheless. Separating facts that are about the subset relation from the more general version of Zorn's lemma would make sense for at least one purpose: reusing the former in developments that use a different definition of partial order (and that are incompatible with the latter). As to the point that a split would make examination of past versions more difficult. How do you mean? True, it would be hard to compare a version that comes somewhere after the split with one somewhere before the split (via plain diff), but how often does that happen? Isn't the typical use-case comparison of successive changesets? cheers chris On 02/27/2013 08:49 PM, Lawrence Paulson wrote: I don't see the point of splitting Zorn into multiple files. It isn't especially large. Such a change really has nothing to do with the question of locating proved results, and it would make it harder to examine past versions. Larry On 27 Feb 2013, at 05:57, Christian Sternagel c.sterna...@gmail.com /mc/compose?to=c.sterna...@gmail.com wrote: Dear all, in the meanwhile I had a close look at the existing Zorn.thy (mostly to understand the proof myself) and came up with the following proposal: see https://bitbucket.org/csternagel/zorns-lemma-and-the-well-ordering-theorem/ for the related hg repository (from which you will hopefully merge into the Isabelle repo ;)). I propose the following changes to ~~/src/HOL/Cardinals and ~~/src/HOL/Library. 1) Make facts about the ordinal sum available in a separate theory, to avoid too early dependency on the old ~~/src/HOL/Library/Zorn. This is a prerequisite to make the remainder of my proposal work. (see Ordinal_Sum.thy) 2) Split the current Zorn.thy into three separate parts. - Zorn_Subset.thy Here we are only concerned with the special case of Zorn's lemma for the subset relation. This constitutes a modernized version of the old Zorn.thy, employing locales for structuring (cf. Andrei's rel locale in ~~/src/HOL/Cardinals; I find this kind of structuring very convenient) and only Isar proofs (some of the old apply scripts were very brittle, e.g., using auto or simp as initial proof steps
Re: [isabelle-dev] Zorn's lemma, the well-ordering-theorem, and extending well-founded relations to (total) well-orders
Dear Larry please note that my proposal is not just about a split of the existing theory Zorn.thy, but also about a modernization of part of it (which I think makes it easier to understand, but I might be wrong... could be that the main purpose of this experiment was just to make me understand the formalized proofs ;)) as well as adding new facts (the order-extension principle). So please consider it, even if no split is done. Nevertheless. Separating facts that are about the subset relation from the more general version of Zorn's lemma would make sense for at least one purpose: reusing the former in developments that use a different definition of partial order (and that are incompatible with the latter). As to the point that a split would make examination of past versions more difficult. How do you mean? True, it would be hard to compare a version that comes somewhere after the split with one somewhere before the split (via plain diff), but how often does that happen? Isn't the typical use-case comparison of successive changesets? cheers chris On 02/27/2013 08:49 PM, Lawrence Paulson wrote: I don't see the point of splitting Zorn into multiple files. It isn't especially large. Such a change really has nothing to do with the question of locating proved results, and it would make it harder to examine past versions. Larry On 27 Feb 2013, at 05:57, Christian Sternagel c.sterna...@gmail.com wrote: Dear all, in the meanwhile I had a close look at the existing Zorn.thy (mostly to understand the proof myself) and came up with the following proposal: see https://bitbucket.org/csternagel/zorns-lemma-and-the-well-ordering-theorem/ for the related hg repository (from which you will hopefully merge into the Isabelle repo ;)). I propose the following changes to ~~/src/HOL/Cardinals and ~~/src/HOL/Library. 1) Make facts about the ordinal sum available in a separate theory, to avoid too early dependency on the old ~~/src/HOL/Library/Zorn. This is a prerequisite to make the remainder of my proposal work. (see Ordinal_Sum.thy) 2) Split the current Zorn.thy into three separate parts. - Zorn_Subset.thy Here we are only concerned with the special case of Zorn's lemma for the subset relation. This constitutes a modernized version of the old Zorn.thy, employing locales for structuring (cf. Andrei's rel locale in ~~/src/HOL/Cardinals; I find this kind of structuring very convenient) and only Isar proofs (some of the old apply scripts were very brittle, e.g., using auto or simp as initial proof steps). Hopefully it is also easier to understand than the old scripts (or maybe it is just because I spend so much time with the proofs ;)). - Zorn.thy The general version of Zorn's lemma for arbitrary partial orders. - Well_Ordering_Theorem.thy The well-ordering-theorem. It seems important enough to give it it's own theory. Moreover, in the previous setup it seemed to be easily overlooked (not even some Isabelle veterans knew whether it was already formalized). 3) Add a formalization of the well-order extension theorem to ~~/src/HOL/Library. (see Well_Order_Extension.thy) In My_Zorn.thy it is illustrated that the new structure is more versatile than the old one. It is, e.g,. very easy to combine it with my alternative definitions of partial orders (po_on from AFP/Well_Quasi_Orders/Restricted_Predicates). cheers chris On 02/21/2013 01:58 PM, Christian Sternagel wrote: Dear all, how about adding Andrei's proof (discussed on isbelle-users) to HOL/Library (or somewhere else)? I polished the latest version (see attachment). cheers chris PS: In case you are wondering: Why is he interested in these results? Here is my original motivation: In term rewriting, termination tools employ simplification orders (like the Knuth-Bendix order, the lexicographic path order, ...) whose definition is often based on a given well-partial-order as precedence. However, termination tools typically use well-founded partial orders as precedences. Thus we need to be able to extend a given well-founded (partial order) relation to a well-partial-order when we want to apply the theoretical results about simplification orders to proofs that are generated by termination tools. (Since every total well-order is also a well-partial-order, this is possible by the above mentioned results.) ___ 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] Extending well-founded relations to (total) well-orders
Dear all, how about adding Andrei's proof (discussed on isbelle-users) to HOL/Library (or somewhere else)? I polished the latest version (see attachment). cheers chris PS: In case you are wondering: Why is he interested in these results? Here is my original motivation: In term rewriting, termination tools employ simplification orders (like the Knuth-Bendix order, the lexicographic path order, ...) whose definition is often based on a given well-partial-order as precedence. However, termination tools typically use well-founded partial orders as precedences. Thus we need to be able to extend a given well-founded (partial order) relation to a well-partial-order when we want to apply the theoretical results about simplification orders to proofs that are generated by termination tools. (Since every total well-order is also a well-partial-order, this is possible by the above mentioned results.) Well_Order_Extension.thy Description: application/example ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Order Relations
On 02/19/2013 03:49 PM, Tobias Nipkow wrote:
Am 19/02/2013 03:50, schrieb Christian Sternagel:
I'm not sure how much work it would be to use this new definition of
reflexivity. But if people think that what I say makes sense (or is more natural
as reflexivity), I would give it a try and report afterwards.
It sounds plausible to me, and I would be in favour of such a change assuming
that your application profits from it and the distribution does not suffer.
Well, currently my applications are all just based on different
definitions than those of Main, so there would be no direct gain.
Moreover, relations are represented by ('a * 'a) set in some places,
whereas 'a = 'a = bool (which I prefer, for some reason I'm not
quite able to put my finger on) is used in others.
In an ideal Isabelle/world I would expect a single definition of
reflexivity that is applicable everywhere and a clear convention for the
type of relations (including orderings) that is used uniformly (or at
least primarily). See. e.g., Ordering.thy vs. Relation.thy for the
current status.
I know that this might not be feasible right now, but who knows, with a
lot of small changes in the long run, it might be doable eventually?
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Order Relations
On 02/18/2013 11:31 PM, Tobias Nipkow wrote: Am 18/02/2013 15:10, schrieb Lawrence Paulson: These definitions originate in Isabelle/ZF, where it is quite essential to have a condition such as r = A * A, because otherwise no reflexive r could exist. They aren't is obviously necessary in Isabelle/HOL, but nevertheless the idea that the domain type can be identified with the actual domain of a relation is inflexible in many applications, where it's essential to have a separate carrier set, a subset of the full type. I believe it was me who ported those definitions. I vaguley recall that I tried various alternatives but this one seemed to work best for the theory at hand, Zorn. I am completely open to a nicer definition but would not want to redo all the proofs that depend on it myself. My main problem with the current definition is that it is not (just) reflexivity, but rather reflexivity plus an additional property (that ensures that a relation is only defined on a domain). Why not split these in two separate predicates and use the second one only where really necessary? I'm not sure how much work it would be to use this new definition of reflexivity. But if people think that what I say makes sense (or is more natural as reflexivity), I would give it a try and report afterwards. cheers chris Tobias And of course, even if they aren't ideal, I'm afraid that we are stuck with them; at least, I suspect that changing them now would be more trouble than it is worth. Larry On 18 Feb 2013, at 05:45, Christian Sternagel c.sterna...@gmail.com wrote: Dear Larry, Stefan, Tobias, and Andrei (as authors of the relevant Isabelle/HOL theories), already several times I stumbled upon the definition of Relation.refl_on (and thus also Order_Relation.Refl) and was irritated. What is the reason for demanding r = A * A? And why are other properties from Order_Relation, which indicate an explicit domain by their name, defined by means of corresponding properties with implicit domain? E.g., in the following definitions definition preorder_on A r == refl_on A r ∧ trans r definition partial_order_on A r == preorder_on A r ∧ antisym r definition linear_order_on A r == partial_order_on A r ∧ total_on A r definition strict_linear_order_on A r == trans r ∧ irrefl r ∧ total_on A r definition well_order_on A r == linear_order_on A r ∧ wf(r - Id) I would expect properties like trans_on, antisym_on, irrefl_on, and wf_on with explicit domain (of course that would only make sense after dropping r = A * A from the definition of refl_on, since otherwise r will only ever relate elements of A in the above definitions). Now I saw that Andrei writes Refl_on A r requires in particular that r = A * A, and therefore whenever Refl_on A r, we have that necessarily A = Field r. This means that in a theory of orders the domain A would be redundant -- we decided not to include it explicitly for most of the tehory. in his README to the new Cardinal theories. So this (strange?) definition of reflexivity is here to stay and used by an ever growing body of theories. This occasionally causes me some headache when I start to think about how my definitions from the AFP entry Well_Quasi_Orders would fit in as standard definitions in Isabelle/HOL. ( do recall that the current definition of Relation.refl_on would not have worked for my proofs.) Any comments are appreciated. 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 ___ 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] Order Relations
Dear Larry, Stefan, Tobias, and Andrei (as authors of the relevant Isabelle/HOL theories), already several times I stumbled upon the definition of Relation.refl_on (and thus also Order_Relation.Refl) and was irritated. What is the reason for demanding r = A * A? And why are other properties from Order_Relation, which indicate an explicit domain by their name, defined by means of corresponding properties with implicit domain? E.g., in the following definitions definition preorder_on A r == refl_on A r ∧ trans r definition partial_order_on A r == preorder_on A r ∧ antisym r definition linear_order_on A r == partial_order_on A r ∧ total_on A r definition strict_linear_order_on A r == trans r ∧ irrefl r ∧ total_on A r definition well_order_on A r == linear_order_on A r ∧ wf(r - Id) I would expect properties like trans_on, antisym_on, irrefl_on, and wf_on with explicit domain (of course that would only make sense after dropping r = A * A from the definition of refl_on, since otherwise r will only ever relate elements of A in the above definitions). Now I saw that Andrei writes Refl_on A r requires in particular that r = A * A, and therefore whenever Refl_on A r, we have that necessarily A = Field r. This means that in a theory of orders the domain A would be redundant -- we decided not to include it explicitly for most of the tehory. in his README to the new Cardinal theories. So this (strange?) definition of reflexivity is here to stay and used by an ever growing body of theories. This occasionally causes me some headache when I start to think about how my definitions from the AFP entry Well_Quasi_Orders would fit in as standard definitions in Isabelle/HOL. ( do recall that the current definition of Relation.refl_on would not have worked for my proofs.) Any comments are appreciated. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] introduction to Isabelle/jEdit for PG users?
Please consult the attached file for a first suggestion for the overview page. (Just to make sure that I'm on the right track; if so I will continue tomorrow ... today my wife won't allow ;); comments are most welcome.) cheers chris On 01/25/2013 09:21 PM, Lawrence Paulson wrote: One option is simply for me to update my existing PG-based preview to use Isabelle/jEdit. At the same time, Christian could perhaps make a webpage by extracting the most important points from his paper. Does this idea makes sense? Larry On 25 Jan 2013, at 10:16, Makarius makar...@sketis.net wrote: On Fri, 25 Jan 2013, Christian Sternagel wrote: It might be good to consolidate your main points in a much shorter webpage. Your paper is structured (naturally) as a paper, but for the corresponding webpage I would delete the abstract and most of the introductory material. I wouldn't actually state that Isabelle/jEdit is awesome (such judgements are always up to the reader), but simply outline what the document model is, and how it differs from approaches used in other systems. I agree. Unfortunately, I will not have time to work on it until February 4 (due to paper deadlines). When is the rollout of Isabelle2013 planned? Approx. 1 week after the ITP deadline, plus a few more days maybe. In these remaining weeks, the priority for me is to sort out issues of the release candidates. As I've told Larry already privately, I welcome his initiative, and already suggested to think about the http://isabelle.in.tum.de/overview.html slot instead of the README. Thus the content can be finalized after the release, even updated occasionally until the next release. Another point. Since we are currently testing release candidates of Isabelle/jEdit and thus there are still chances of changes, it might be good to wait with any tutorial, until the testing phase is over? I don't plan substantial changes, just sorting out oddities that can be sorted out, without endangering the system integrity in the last moment. Makarius Title: Overview Overview · · Navigation Home Overview Installation Documentation Community Site Mirrors: Cambridge(.uk) Munich(.de) Sydney(.au) What is Isabelle? Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols. A bluffer's glance at Isabelle content The Isabelle/jEdit user interface Isabelle/jEdit provides an interaction model where the user sees and freely edits a document. All the heavy machinery of Isabelle, like proof checking and proof search, asynchronously runs in the background and supplies the document with semantic information that is presented in standard ways (highlighting, hyperlinks, tooltips, etc.). Proof General: We have a visible locked region that can be extended or reduced. That is, a user can only step sequentially through a document. This model of interaction offers plenty of space for parallelization. Thus, Isabelle/jEdit does not only provide a more modern user interface but additionally facilitates to transparently (for the user) make use of multi-core architectures. Getting started Isabelle/jEdit is part of the official Isabelle release. To use it, just follow the installation instructions. To start Isabelle/jEdit from a command line use something similar to $ISABELLE_HOME/bin/isabelle jedit (On MacOSX click on the Isabelle2013.app icon and select Isabelle/jEdit; on windows click Isabelle2013.exe.) On the top half is the main buffer, this is where source text is shown and editing takes place. At the bottom of the lower half there are (among others) the buttons Output and README. By default README is selected, which gives some useful information. When selecting Output, the panel shows the output buffer. This is where messages from the command on which the cursor is positioned can be found. Part of the right margin is the button Theories, whose corresponding panel can be consulted to check whether Isabelle/jEdit agrees with you on what files are loaded and how much of them (problems are indicated in red). To start using Isabelle/jEdit let us formalize a simple fact about lists. Before doing so, we need to start a theory (Isabelle
Re: [isabelle-dev] introduction to Isabelle/jEdit for PG users?
I just noticed that the first few lines of the text on index.html and overview.html are identical. That's a bit odd. cheers chris On 02/15/2013 03:27 PM, Christian Sternagel wrote: Here is what I came up with. I merged it with the text of the existing overview.html (from there I just dropped the two sentences about PG and jEdit). On 02/14/2013 09:32 PM, Lawrence Paulson wrote: It's looking good, but my personal suggestion is to keep it short. I suspect you may be wanting to run away with it a little. Feel free to drop, move, or modify anything you want (e.g., the example session could be on a separate page). cheers chris I hope to update my old animated presentation, based on Proof General, when I get a little time. Larry On 14 Feb 2013, at 08:21, Christian Sternagel c.sterna...@gmail.com wrote: Please consult the attached file for a first suggestion for the overview page. (Just to make sure that I'm on the right track; if so I will continue tomorrow ... today my wife won't allow ;); comments are most welcome.) cheers chris On 01/25/2013 09:21 PM, Lawrence Paulson wrote: One option is simply for me to update my existing PG-based preview to use Isabelle/jEdit. At the same time, Christian could perhaps make a webpage by extracting the most important points from his paper. Does this idea makes sense? Larry On 25 Jan 2013, at 10:16, Makarius makar...@sketis.net wrote: On Fri, 25 Jan 2013, Christian Sternagel wrote: It might be good to consolidate your main points in a much shorter webpage. Your paper is structured (naturally) as a paper, but for the corresponding webpage I would delete the abstract and most of the introductory material. I wouldn't actually state that Isabelle/jEdit is awesome (such judgements are always up to the reader), but simply outline what the document model is, and how it differs from approaches used in other systems. I agree. Unfortunately, I will not have time to work on it until February 4 (due to paper deadlines). When is the rollout of Isabelle2013 planned? Approx. 1 week after the ITP deadline, plus a few more days maybe. In these remaining weeks, the priority for me is to sort out issues of the release candidates. As I've told Larry already privately, I welcome his initiative, and already suggested to think about the http://isabelle.in.tum.de/overview.html slot instead of the README. Thus the content can be finalized after the release, even updated occasionally until the next release. Another point. Since we are currently testing release candidates of Isabelle/jEdit and thus there are still chances of changes, it might be good to wait with any tutorial, until the testing phase is over? I don't plan substantial changes, just sorting out oddities that can be sorted out, without endangering the system integrity in the last moment. Makarius overview.html ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle.in.tum.de web server encoding
Just as a further data point: when visiting http://isabelle.in.tum.de/website-Isabelle2013-RC2/dist/Isabelle2013-RC2/CONTRIBUTORS using firefox (on Linux) where the default encoding on the client side is Western ISO-8859-1 then some symbols are strange. If I explicitly set the encoding to Unicode UTF-8, everything seems fine. cheers chris On 02/06/2013 09:20 PM, Makarius wrote: Dear Apache experts, some days ago I noticed the famous French problem http://www.apprendre-en-ligne.net/bloginfo/index.php/2009/01/21/151-martine-ecrit-en-utf-8 on the TUM web server. This affects names in http://isabelle.in.tum.de/website-Isabelle2013-RC2/dist/Isabelle2013-RC2/CONTRIBUTORS for example. Right now I don't see it, maybe because it is due to a different web client configuration on my side. In principle, the local config-tum repository should tell about the situation, but I am unsure where is the right spot to tell Apache using UTF-8 encoding by default. 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] Fork of Isabelle2013 release repository TODAY
Dear Gerwin, Its already a bit late for my idea and maybe I'm the only one in that situation, but at least for me it would make sense to wait with the AFP release until the paper submission deadline of ITP. (Since the dates are rather close anyway and ITP submissions should be accompanied by links to formalizations, having a release entry, rather than a development entry, would be nice.) Of course I can also send any later changes by email (as you suggest below), but if others are in a similar situation, you might save some work by waiting a bit longer. cheers chris PS: By the same token, an option to submit to the release branch around the deadline of the camera ready version (in case of acceptance *fingers crossed*) would also be nice (in case, reviews triggered changes in a formalization). Anyone else? On 01/22/2013 06:33 AM, Gerwin Klein wrote: On 21.01.2013, at 2:08 AM, Makarius makar...@sketis.net wrote: * AFP needs to be understood wrt. isabelle-release. Gerwin will explain his organization of the AFP release for Isabelle2013, based on the afp-devel repository. I'll attempt to make the AFP release semi-simultaneous with the Isabelle release this time. This means, afp-test will point to the Isabelle release candidate by Fri morning SYD time (Thu night CET). At the same time (Thu night CET), the afp release branch will fork in afp-devel. Any commits after will not be visible in the 2013 AFP release unless you specifically send them to me by email. If there are any updates/cleanups/last minute changes yet to be done for any of the entries, please have them in by then. Cheers, Gerwin The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ 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] introduction to Isabelle/jEdit for PG users?
Dear Larry, On 01/25/2013 12:19 AM, Lawrence Paulson wrote: There is a lot of useful information in this paper! I think I have finally got the point of the document model. Good to hear. It might be good to consolidate your main points in a much shorter webpage. Your paper is structured (naturally) as a paper, but for the corresponding webpage I would delete the abstract and most of the introductory material. I wouldn't actually state that Isabelle/jEdit is awesome (such judgements are always up to the reader), but simply outline what the document model is, and how it differs from approaches used in other systems. I agree. Unfortunately, I will not have time to work on it until February 4 (due to paper deadlines). When is the rollout of Isabelle2013 planned? At some point makarius also suggested a screencast tutorial video for jEdit (I gather you had something similar for emacs once). I'm still interested in contributing to that (but the same time constraints as above apply). I'm not sure if such a screencast should/could be part of the Isabelle distribution, though. If not, time is not constrained by the upcoming Isabelle release. Another point. Since we are currently testing release candidates of Isabelle/jEdit and thus there are still chances of changes, it might be good to wait with any tutorial, until the testing phase is over? It might be good to keep the Proof General material separate, e.g. as a sidebar (assuming we make a webpage). Other users might be coming from systems such as Coq, which behave very differently, whether or not Proof General is involved. The other option is to put something like this right in Isabelle/jEdit's README file. Frankly I think the current version isn't that useful to beginners, and they are the main target of any README file. cheers chris Larry On 23 Jan 2013, at 00:19, Christian Sternagel c.sterna...@gmail.com wrote: I tried to summarize most of the issues that made it to the Isabelle mailing lists (at that time) in my submission to the Isabelle Users Workshop. http://arxiv.org/abs/1208.1368 It's definitely incomplete, but maybe it could help. cheers chris On 01/23/2013 04:07 AM, Tobias Nipkow wrote: In principle a good idea, but I don't think we want multiple intros for different audiences. Hence I would aim for a general intro that also covers points that PG users are used to. Tobias Am 22/01/2013 13:30, schrieb Lawrence Paulson: Do we provide an introduction to Isabelle/jEdit for PG users? It might be a good idea to do so. I'm willing to make a first attempt at this, though I'm sure it will contain some mistakes, which I'm sure others of you would be only too happy to fix. I have in mind a single webpage, with a couple of screenshots. In fact, I don't know the full possibilities of Isabelle/jEdit, so it will only be a start. But as usual, the first step seems to be the hardest. 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 ___ 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] introduction to Isabelle/jEdit for PG users?
I tried to summarize most of the issues that made it to the Isabelle mailing lists (at that time) in my submission to the Isabelle Users Workshop. http://arxiv.org/abs/1208.1368 It's definitely incomplete, but maybe it could help. cheers chris On 01/23/2013 04:07 AM, Tobias Nipkow wrote: In principle a good idea, but I don't think we want multiple intros for different audiences. Hence I would aim for a general intro that also covers points that PG users are used to. Tobias Am 22/01/2013 13:30, schrieb Lawrence Paulson: Do we provide an introduction to Isabelle/jEdit for PG users? It might be a good idea to do so. I'm willing to make a first attempt at this, though I'm sure it will contain some mistakes, which I'm sure others of you would be only too happy to fix. I have in mind a single webpage, with a couple of screenshots. In fact, I don't know the full possibilities of Isabelle/jEdit, so it will only be a start. But as usual, the first step seems to be the hardest. 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proposing extensions to the Isabelle library?
Dear Alessandro, sorry for the late answer. I can only tell you what I usually do (which does not mean that it is the best thing to do... maybe one of the developers could comment which way is the most convenient one for adopting external changes). * I use 'hg qpop; hg pull; hg update; hg qpush' (I guess that is equivalent to 'hg qpop; hg pull -u; hg qpush'; the reason for not using --rebase is that I want to avoid any modification of the repository history, even for my local clone) * For the same reason I do not qfinish a patch before I submit it to the mailing list ... since it could pollute my local history (I think). Instead I wait until the change is adopted by somebody with push access, then pull again from the Isabelle repo and delete my local patch. What I send to the mailing list is just the patch file which is stored at .hg/patches/ (under the name that you chose for your patch). cheers chris PS: I did not always proceed as described above (and already caused some unnecessary changes in the history)... this is just my latest try. I hope it's not a bad one ;) On 01/07/2013 06:39 AM, Alessandro Coglio wrote: Hi Christian, Thank you very much for the helpful information. Using mq sounds like a good idea. I have some familiarity with hg, but none with mq. I looked at some documentation, but I was wondering if you could quickly point me in the right direction: * Assuming I'll be working with just one patch, should I update from upstream by doing 'hg pull --rebase' or 'hg qpop; hg pull -u; hg qpush'? Or in some other way? * Once I have a completed, qrefreshed patch that builds with the latest changesets from upstream, should I qfinish it (which, if I understand, generates a local commit) or not? How do I package this patch to send it to the isabelle-dev mailing list -- via 'hg bundle' or in some other way? Thanks! On 12/28/12 5:10 AM, Christian Sternagel wrote: Dear Alessandro, the necessary steps are outlined in the community wiki, here https://isabelle.in.tum.de/community/Publish_contributions_as_an_external Since the status of the wiki is not clear at the moment. I summarize the steps also in this e-mail for later reference. 0) confirm with any of the isabelle developers that your work would be appreciated and pushed after you finished (you already did that) 1) consult http://isabelle.in.tum.de/repos/isabelle/file/tip/README_REPOSITORY for how to work with the development repo (as well as conventions, e.g., for mercurial commit messages etc.) 2) testing changes: Before publication, pull any changes from the official repository. (This might effect a merge.) Now test your changes at least by isabelle build -a -o browser_info -o document=pdf -o document_graph 3) The archive of formal proofs is a separate mercurial repository (which also has a development version). Often, this is adapted by some isabelle developer (you have to confirm this). Otherwise you would have to checkout this repo and test it against your changes yourself. 4) Creating a bundle: Packaging your changes into a single file can be done with hg bundle somefilename.hgbundle 5) Publishing contributions: Finally, the previously created bundle can be sent to someone with push access to the Isabelle main repository, either directly (assuming mutual agreement) or indirectly via the mailing list. An alternative is exchange through an external repository service like github. hope this helps, cheers chris PS: personally I found the mq extension of mercurial (for patch queues) very helpful. Using mq I can collect all my changes as patches (that are not commited to the repo) as well as continuously update the repo from upstream. At the end I just send a patch to the mailing list (without ever changing the history besides the final commit that is done by a developer). On 12/28/2012 07:59 AM, Alessandro Coglio wrote: Hi Florian, I followed the instructions and things seems to be working fine in my clone of the repo. Before I start trying out the change outlined in your email, I'd like to double-check a few things: * In order to modify Orderings and other theories that are part of Main, I should start Isabelle with the '-l Pure' option and load/change the files manually, correct? * Once Main runs fine, I should check/change any files under the src/HOL tree that may depend on Orderings. Does any file under the other src/... trees depend on anything under the src/HOL tree? * Is the successful completion of 'isabelle build -a' the final criterion for determining that everything has been modified correctly? I didn't see any separate test suites in the repo. * Should the AFP (which I didn't see in the repo) be checked/changed as well? Or is it updated only when there is a release? Thanks! On 12/22/12 4:01 AM, Alessandro Coglio wrote: Hi Florian, I'd be happy to contribute, so I'll look into that. I don't have a lot of spare
Re: [isabelle-dev] Proposing extensions to the Isabelle library?
Dear Alessandro, the necessary steps are outlined in the community wiki, here https://isabelle.in.tum.de/community/Publish_contributions_as_an_external Since the status of the wiki is not clear at the moment. I summarize the steps also in this e-mail for later reference. 0) confirm with any of the isabelle developers that your work would be appreciated and pushed after you finished (you already did that) 1) consult http://isabelle.in.tum.de/repos/isabelle/file/tip/README_REPOSITORY for how to work with the development repo (as well as conventions, e.g., for mercurial commit messages etc.) 2) testing changes: Before publication, pull any changes from the official repository. (This might effect a merge.) Now test your changes at least by isabelle build -a -o browser_info -o document=pdf -o document_graph 3) The archive of formal proofs is a separate mercurial repository (which also has a development version). Often, this is adapted by some isabelle developer (you have to confirm this). Otherwise you would have to checkout this repo and test it against your changes yourself. 4) Creating a bundle: Packaging your changes into a single file can be done with hg bundle somefilename.hgbundle 5) Publishing contributions: Finally, the previously created bundle can be sent to someone with push access to the Isabelle main repository, either directly (assuming mutual agreement) or indirectly via the mailing list. An alternative is exchange through an external repository service like github. hope this helps, cheers chris PS: personally I found the mq extension of mercurial (for patch queues) very helpful. Using mq I can collect all my changes as patches (that are not commited to the repo) as well as continuously update the repo from upstream. At the end I just send a patch to the mailing list (without ever changing the history besides the final commit that is done by a developer). On 12/28/2012 07:59 AM, Alessandro Coglio wrote: Hi Florian, I followed the instructions and things seems to be working fine in my clone of the repo. Before I start trying out the change outlined in your email, I'd like to double-check a few things: * In order to modify Orderings and other theories that are part of Main, I should start Isabelle with the '-l Pure' option and load/change the files manually, correct? * Once Main runs fine, I should check/change any files under the src/HOL tree that may depend on Orderings. Does any file under the other src/... trees depend on anything under the src/HOL tree? * Is the successful completion of 'isabelle build -a' the final criterion for determining that everything has been modified correctly? I didn't see any separate test suites in the repo. * Should the AFP (which I didn't see in the repo) be checked/changed as well? Or is it updated only when there is a release? Thanks! On 12/22/12 4:01 AM, Alessandro Coglio wrote: Hi Florian, I'd be happy to contribute, so I'll look into that. I don't have a lot of spare time, so it may take me a while. The Jan or Feb release is safe :) On 12/18/12 12:18 PM, Florian Haftmann wrote: Hi Alessandro, Is there any plan to make things in the library more uniform (one way or the other)? Is there a preference for new type classes should be developed (purely syntactic or with assumptions)? well, there is no big masterplan. Usually things evolve: somebody thinks about an extended or more fine-grained hierarchy and thinks how to accomplish things without breaking more than necessary. Personally, I like syntactic classes because they are more modular. For example, in the library extensions that I sent the other day, the definition of type class finite_lattice_complete would be perhaps slightly cleaner if bot and top were syntactic classes like Inf and Sup. Just my 2 cents. I.e. something like class bot ~ class order_bot class top ~ class order_top class bot = fixes bot :: 'a class top = fixes top :: 'a Could make sense. The question is whether somebody is willing to undertake this change. If you would consider this, you find the first clues at http://isabelle.in.tum.de/repos/isabelle/file/c5e0073558f3/README_REPOSITORY. Get back here if questions remain. Note that currently we are heading towards a next release in January or February, and time might be too terse to polish and incorporate a change like the one sketched above. Hope this helps, 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] 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 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 = cctx.filenode('.hgtags')
File
Re: [isabelle-dev] Must the AFP be used as a component?
Dear all, I think I already used the $AFP in my original submission. The reason was that having such a variable seemed more robust to me than just having a relative ../ (so a user could put the entry anywhere he wants). Sorry for the confusion. cheers chris On 12/14/2012 07:18 PM, Gerwin Klein wrote: On 14/12/2012, at 6:55 PM, Lars Noschinski nosch...@in.tum.de wrote: The reason is that Open_Induction/ROOT (and also Open_Induction/Open_Induction.thy) relies on $AFP being set, which is only the case if AFP is registered as a component (which is not the case for Mira). @Gerwin: Since you made the ROOT file, what was the intention of using $AFP instead of ../ used in all other theories? I think I was just experimenting with the new build system. Not a successful experiment, it seems. I'll change it to the usual ../ Cheers, Gerwin The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ 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
