Re: [isabelle-dev] Remaining uses of Proof General?
Hi Makarius, On Thu, Jun 26, 2014 at 11:08 PM, Makarius wrote: > At the moment (06599233e54e) there are no remaining uses of Proof General to > the best of my knowledge. If anybody has counter-examples they should be > put on the table for discussion. I am using Isabelle via ProofGeneral on a server without X. I do not know of a way to run JEdit without X. Some of my uses of Isabelle need as much as 100GB memory (and I also make use of the parallelization to much more CPUs than my laptop has), so I need to work sshed to the server. Cheers, Cezary > > Makarius > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- Cezary Kaliszyk, University of Innsbruck, http://cl-informatik.uibk.ac.at/~cek/ ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New HOL/Import
On Thu, Mar 29, 2012 at 8:04 PM, Makarius wrote: > Wow, I am impressed by the brevity of it. You should mention the secret > http://cl-informatik.uibk.ac.at/~cek/proofs which is a bzip stream to be > uncompressed, before it can be used with import_file in the example. That's the preprocessed proof image for importing basic hol-light. > You are no longer using any XML/YXML now. Is the format somehow related to > OpenTheory by Joe Hurd? No; the information stored is similar to the old format, but more brief and easier to parse: every line contains a next typ/term/thm to read, with arguments space separated and last uses of an object marked with a minus. It could be converted (possibly automatically) to OpenTheory; however the sharing is done at a different level so it would be hard to recover additional sharing and without it, Opentheory would be at least an order of magnitude bigger. >> - Does anyone have opinions about the HOL4 code that has been long dead? > Which HOL4 code do you mean exactly? The code currently in isabelle repository is in 3 places: Import, Import/HOL_Light and Import/HOL4 The Import/HOL_Light is functional but the proposed code replaces it. The Import/HOL4 has not been functional for a while, (I have not been able to use it even with proofs from 2004); should it still stay in the repository? Regards, Cezary ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] New HOL/Import
Hi all, We have been working on a modernized reimplementation of HOL/Import, for HOL Light. We think we are at a point where it could be pushed to the main Isabelle repository replacing the old one. Therefore two questions: - Is anyone using the old HOL/Import? - Does anyone have opinions about the HOL4 code that has been long dead? Most important changes in the new importer as opposed to the old one: - It is much more scalable. Regular HOL-Light can be imported in less than a minute. Importing bigger theories works as well. - Rather than generating 'thy' files it creates an Image file and documentation, see either of the below: http://cl-informatik.uibk.ac.at/~cek/import.html http://cl-informatik.uibk.ac.at/~cek/import.pdf - The code is shorter and cleaner. For those that would like to inspect the code it is at: http://cl-informatik.uibk.ac.at/~cek/import.tgz Regards, Cezary -- Cezary Kaliszyk, University of Innsbruck, http://cl-informatik.uibk.ac.at/~cek/ ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Status of HOL/Import
Hi Florian, On Sun, Mar 04, 2012 at 10:15:38AM +0100, Florian Haftmann wrote: > I've been working on the Importer stuff, not very deeply, but separating > HOL4 and HOL Light contents, stripping generic parts of any name > reference to HOL4, etc. [...] Great! > There could be done a lot more on the ML stuff to introduce basic coding > practice there, of course, but for the moment I will leave that aside. As I mentioned to you privately, we (w Alex) are trying to write a new better import. So before working on the old one too much, lets first see which parts are reused and which will not. > Two questions: > a) There is a README; maybe you would like to update it according to > your current expertise? > b) After the pred/set issue, the generated HOL Light theories must be > regenerated. Do you have time to accomplish this? Alternatively, I > could follow the README instructions as soon as available. There are two issues; first: This is not as straightforward as it seems; apparently some of the constant maps have types that are not valid anymore (for example INSERT), so it is not going to work immediately. One can update it with most of the constant maps removed immediately; but I would suggest waiting a week or two for the new import and trying to get the maps correct there. But more importantly, the concept of generating these files and then replaying them with 'sorrys' is very strange in an LCF approach. Having built the session once, one can checkpoint the image and this is much nicer than the generated sources. The only thing this needs instead is some way to generate documentation. Makarius once suggested an antiquotation, that does something like 'print_theorems'. I have not investigated how to implement one? Cheers, Cezary ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quotient example with partiality?
Hi Florian, All, 2011/11/29 Florian Haftmann : > I'm asking myself the question how one would define rational numbers > using the quotient package. The key issue is that the equivalence > relation here is partial, ruling out denominators of value zero. In the > Isabelle reference manual I can find »partial:« in a syntax diagram but > not any concrete example in the distribution. When developing the quotient package we included the infrastructure for defining quotient types with partial equivalence relations, however since one of the main uses was supposed to be nominal (where its always reflexive) we did not test the partial functionality too much. The idea of using the quotient package with partial equivalence relations is that two changes need to be done: First if the user specifies 'partial:' in the quotient_type definition, the obligation to prove changes from 'equivp' to 'part_equivp'. Which is simpler, but then less lifting can be done automatically (to be more precise, some of the theorems that allow for automatic regularization do hold only for reflexive equivalence relations). Second, when lifting theorems, the theorems on the raw level can talk about elements being in the domain (the reflexive part of the partial equivalence relation). This is achieved by quantifying the variables with bounded quantifiers that respect the partial equivalence relation. These should then be lifted to quantifiers over the lifted type. Having said this, we did not develop any examples where the relation would be a real partial equivalence, we only tried to use 'partial' with reflexive equivalence relations. I will try to draft an example partial quotient and get back to you. As for the second question, yes quotients do more than typedef so I am also confused as to the reasons for mixing the two. It would be nice to get it fully localized but still the meaning of typedef that restricts a type fixed in a locale is quite unclear. Or has this been cleared in the meantime? Regards, Cezary ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Fri, Aug 26, 2011 at 5:45 AM, Florian Haftmann < florian.haftm...@informatik.tu-muenchen.de> wrote: > > [...] According to my knowledge, the following session produce > problems: [...] > HOL-Quotient_Examples FAILED > Please propagare the isabelle changeset: http://isabelle.in.tum.de/repos/isabelle/rev/5e0f9e0e32fb to Isabelle-set. With it, Quotient_Examples succeeds. Cheers, Cezary ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On Thu, Aug 18, 2011 at 3:49 AM, Florian Haftmann < florian.haftm...@informatik.tu-muenchen.de> wrote: > [...] So, the best way now is > to continue eliminating set-pred mixture (also in the AFP of course!) > and discover problems in packages – I'm a little concerned about > quotient since this has been introduced after 2008, but maybe Cezary can > comment on this. Hi Florian, I already made the changes to the core of the quotient package as of: http://isabelle.in.tum.de/repos/isabelle/rev/3cdc4176638c With the above the quotient package works both as is and with the explicit set type. It seems you included only a part of the above changeset in the isabelle_set repository, in particular the change in the src/HOL/Equiv_Relations.thy is necessary but seems it did not go in. With this change the quotient package works and only changes to the particular examples may be needed, but many work without any changes: New Nominal: Works. Quotient_Message: Works. Quotient_Int: Works. FSet: Requires removing one 'simp add: mem_def', then works. DList: I pushed a change 5 min ago; with it it works. CSet and List_Cset depend on Library/More_Set which doesn't load, so I can't say if there are any quotient issues... AFP/Coinductive needs updating, long before quotients it does: enat_set :: "enat => bool" so I can't say without going further in the code. Regards, Cezary. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testing HOL/Import
On Wed, Jul 20, 2011 at 11:33 AM, Alexander Krauss wrote: > Now my question is: What do we actually know when HOL-Generate-HOLLight > completes without error? Should the generated file be compared with the > version in the repository and should the test fail when they are not > identical? Are there other things that should be checked? Completing without error is already quite good; I am not sure about the file comparison: At the moment there are two generated files, the 'thy' file and the 'imp' file. The 'thy' file has all the theorems that are present in HOL Light but not in Isabelle. The 'imp' file includes theorem mappings. If new things are proved in Isabelle that are identical to the ones that were in HOL-Light, theorems with disappear from the 'thy' file and the mapping in the 'imp' file will refer to the new theorems. This does not sound like a reason for failing? Cezary ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Status of HOL/Import
On Wed, Jul 13, 2011 at 4:51 PM, Alexander Krauss wrote: > On 07/12/2011 11:15 PM, Florian Haftmann wrote: > I just tried to redo this to see how it works > $ svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light > $ cd hol_light/Proofrecording/hol_light > $ make > and it failed with > [...] The issue is with versions of OCaml. The HOL Light distribution includes a number of versions of the parser (files pa_j_XXX.ml) that are supposed to work with particular versions of OCaml. I am using an old version of OCaml for HOL Light (3.10.2) however the distribution includes some pa_j_ files for versions 3.11.XXX. Also make sure that camlp5 has the same version as ocaml; as this is not the case for example on macbroys. One more suggestions, try to run 'make' in the top directory of hol light first; after this works you can copy pa_j.ml and pa_j.cm* to ProofRecodring/hollight. > Also, what is the HOL Light release policy? Is everybody really just using > the svn head? Last named release (2.20) was in 2005, since then John Harrison sometimes packs versions considered "more stable". Otherwise it is the SVN. Cezary ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Status of HOL/Import
Hi Florian, On Wed, Jul 13, 2011 at 6:15 AM, Florian Haftmann wrote: > Of course there is a lot one could clean up. In my eyes there are some > issues which prevent an understanding of HOL-Import »in the large«, and > maybe your experience could answer the following questions: > > a) HOL-Import seems to import both HOL4 and HOL Light, but the ROOT.ML > file > http://isabelle.in.tum.de/reports/Isabelle/file/e84239a47f32/src/HOL/Import/ROOT.ML > only mentions HOL4Compat and HOL4Syntax as imported theories. Where > does HOL Light come in? The setup is indeed confusing and it would be great to change it. Currently IsaMakefile allows for two targets: HOL-Generate-HOL and HOL-Generate-HOLLight (They cannot be called together, so the 'generate' target in the makefile does not make sense). Generate-HOL refers to the ROOT.ML you mentioned. HOLLight refers to a ROOT.ML in a subdirectory: http://isabelle.in.tum.de/reports/Isabelle/file/e84239a47f32/src/HOL/Import/Generate-HOLLight/ROOT.ML Which refers to the HOLLight generation script which uses some of the files from the main Import directory. > b) There seems to be no README or generated document which explains at > least rudimentary how to actually use the importer. Is there any > reference for that? There is a README in HOL-Light source code that explains how to get the recorded proofs: http://hol-light.googlecode.com/svn/trunk/Proofrecording/README With the files generated this way, it is enough to set the HOL4PROOFS environment variable and one can import the generated file or run 'isabelle make HOL-Generate-HOLLight' to regenerate it. This is all I have used. > There is also space for structural improvements; one is mentioned in > the at least parly outdated > http://isabelle.in.tum.de/reports/Isabelle/file/e84239a47f32/src/HOL/Import/HOL/README > it is confusing that files *from* which files are generated are placed > in a directory named »Generate…« and not the other way round. > One could also ask whether generated files must be part of the versioning > anyway. Renaming the files and splitting them into the directories: HOL4, HOLLight, Common and Generated would be a great idea. I would however keep the generated "thy" files in the distribution. It is a collection of 1300 lemmas. without proofs (so they do not take up too much space), that do not exist in Isabelle in this form elsewhere and (as the README says) could be used without getting HOLLight running, exporting the proofs etc. Cheers, Cezary ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Workshop on Mathematical Wikis at ITP 2011 (Nijmegen, NL, August 27; abstract submission May 30)
Workshop on Mathematical Wikis (MathWikis-2011) at ITP (2nd International Conference on Interactive Theorem Proving) 2011 Nijmegen, Netherlands, August 27th, 2011 INVITED SPEAKER: Joe Corneli: The PlanetMath Encyclopedia ABSTRACT SUBMISSION DEADLINE May 30th Mathematics is increasingly becoming a collaborative discipline. The Internet has simplified the distributed development, review, and improvement of large proofs, theories, libraries, and knowledge repositories, also giving rise to all kinds of collaboratively developed mathematical learning resources. Examples include the PlanetMath free encyclopedia, the Polymath collaborative collaborative proof development efforts, and also large collaboratively developed formal libraries. Interactive computer assistance, semantic representation, and linking with other datasets on the Semantic Web are becoming very interesting aspects of collaborative mathematical developments. The ITP 2011 MathWikis workshop aims to bring together developers and major users of mathematical wikis and collaborative and social tools for mathematics. TOPICS include but are not limited to: * wikis and blogs for informal, semantic, semiformal, and formal mathematical knowledge; * general techniques and tools for online collaborative mathematics; * tools for collaboratively producing, presenting, publishing, and interacting with online mathematics; * automation and computer-human interaction aspects of mathematical wikis; * practical experiences, usability aspects, feasibility studies; * evaluation of existing tools and experiments; * requirements, user scenarios and goals. SUBMISSIONS Researchers interested in participating are invited to submit a short (2-10 pages) abstract via EasyChair. Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Submissions should be in standard-conforming Postscript or PDF. To submit a paper, go to the EasyChair MathWikis page (http://www.easychair.org/conferences/?conf=mathwikis11) and follow the instructions there. FINAL VERSIONS Final versions should be prepared in LaTeX using the easychair.cls class file (http://www.easychair.org/easychair.zip). Proceedings will be published as EasyChair or CEUR Workshop Proceedings. IMPORTANT DATES * Submission of abstracts: May 30th, 2011, 8:00 UTC+1 * Notification: June 23rd, 2011 * Camera ready versions due: July 11th, 2011 * Workshop: August 27th, 2011 PROGRAM COMMITTEE * Jesse Alama * David Aspinall * Joe Corneli * Cezary Kaliszyk * Fairouz Kamareddine * Michael Kohlhase * Markus Krötzsch * Christoph Lange (co-chair) * Lionel Mamane * James McKinna * Piotr Rudnicki * Carst Tankink * Josef Urban (co-chair) * Denny Vrandečić ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Document preparation failure
The constant name and theorem name should now be quoted properly
and the documentation builds for me now.
Cezary
On Fri, Feb 19, 2010 at 5:31 PM, Brian Huffman wrote:
> On Fri, Feb 19, 2010 at 8:18 AM, Rafal Kolanski
> wrote:
>> Looks like it should be @{const "apply_rsp"} or @{text "apply_rsp"} or
>> something. The underscore is throwing it.
>
> That's exactly it. There's actually a second problem of the same kind
> later on, in a subsection heading. I have a fix on my local
> repository, and I'll push it as soon as I can rebuild the HOL-Main
> image (assuming it works!)
>
> - Brian
> ___
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
Cezary Kaliszyk kaliszyk at in.tum.de
Nominal Methods Group, Technische Universit?t M?nchen
http://www4.in.tum.de/~kaliszyk/
