Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-02-08

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
02:47 ilbot3 joined #isabelle
02:47 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
04:45 andromeda-galaxy joined #isabelle
04:47 andromeda-galaxy I'm new to Isabelle (still trying to get Gentoo to build the 2015 release, in fact), and was wondering about editor support: I'd like to be able to work on proofs from within emacs (I have a large and well-tuned emacs configuration) but it looks like most of the development has been focused on the jEdit ide.  Is there any emacs interface to the Isabelle/Scala features?
06:51 ammbauer joined #isabelle
07:05 ThreeOfEight andromeda-galaxy: I really don't think you want to go down that road
07:06 ThreeOfEight I don't think there's any emacs support except for what's left of Proof General (and my guess is that Isabelle has changed sufficiently since that was dropped to make it really difficult to get it to work again)
07:06 ThreeOfEight from what I gathered, you would need a very thorough understanding of PIDE and a /lot/ of time to get something like emacs support for Isabelle working again
15:22 andromeda-galaxy ThreeOfEight: okay, thanks for the information.  That's a shame, but I can probably use jEdit if I have to (although I might also check if the old PG supports works, since I think that the Proof General team might have been developing it separately)
15:23 andromeda-galaxy How do you build Isabelle (get every file that it will eventually need in an archive) ahead of time?  I can't find any information on that...
15:42 ThreeOfEight What do you mean by "build"?
15:42 ThreeOfEight Oh you mean like isabelle scala etc?
15:42 ThreeOfEight "isabelle build -b HOL" should probably take care of it
15:43 ThreeOfEight that should buils Isabelle/Scala and the basic images Pure and HOL
15:43 ThreeOfEight *build
15:43 ThreeOfEight but it will put them into ~/.isabelle, I think
15:46 int-e andromeda-galaxy: Afaiu, PG used Isabelle's tty loop which was removed in Isabelle2014. So no, PG will not work.
15:52 ThreeOfEight even as a die-hard Proof General fanboy, I would recommend using jEdit
15:52 ThreeOfEight it's really not so bad once you get used to it
16:02 larsrh As a die-hard jEdit fanboy, I too would recommend using it :-)
16:02 larsrh Once you get used to it PG will seem incredibly backwards
16:03 larsrh That is, PG is a nice piece of engineering, but the interaction model really doesn't work well for interactive proving, IMHO
16:03 ThreeOfEight PG did have vastly superior management of user-defined symbol abbreviations though
16:03 int-e Some interactions like C-hover are awful (but I don't think that's jedit's fault exactly).
16:04 ThreeOfEight and the fact that Isabelle/JEdit always eagerly processes unfinished code and then freezes up are really annoying
16:04 ThreeOfEight *is
16:04 larsrh Wait, is this turning into a PG vs jEdit discussion? I'm getting my pitchfork ready :-)
16:05 larsrh int-e: You mean the need to C-hover to reveal additional markup, such as typing?
16:05 larsrh s/typing/types
16:05 int-e larsrh: no, I mean that C-hover is very awkward to perform.
16:06 int-e (press control, then wiggle the mouse)
16:07 larsrh I think it should be possible to map a keybinding to "open a popup with markup at this position"
16:07 ThreeOfEight Personally, I think the only proper Isabelle IDE is Isabelle/Eclipse
16:07 ThreeOfEight (just trolling)
16:08 larsrh At some point I wanted to implement that, but got sidetracked by other side projects
16:08 int-e But anyway, nobody (including me) is complaining about the huge number of things that actually work well in Isabell/jEdit.
16:50 JCaesar larsrh: I don't think pitchforks are gonna help against emacs. You'll need at least a trident.
16:51 andromeda-galaxy Yeah, Isabelle/jEdit sounds interesting, I'll try it out, thanks for the information.  By build, I meant getting a dist tarball with all the runtime files needed, so that nothing gets unpacked later, since I'm using a package manager (gentoo portage) and want to do a package for Isabelle
16:56 JCaesar andromeda-galaxy: Last time I tried, that lead to an attempted use of over 30GB in /tmp…
16:57 JCaesar Please tell me if you succeed in getting something meaningful.
17:00 tangentstorm is there no way to run isabelle from the command line at all? or just no interactive prompt?
17:05 int-e tangentstorm: there's no interactive prompt. 'isabelle build' for example can be used to build heap images in a shell
17:06 int-e (well, no interactive prompt for proof. there's an ML console, and a scala console)
17:07 int-e for proof -> for doing proofs
17:07 tangentstorm but surely there's some automated way to batch-check a directory of proofs or something, without manually loading each one into the editor?
17:08 int-e yes, isabelle build.
17:18 tangentstorm ah cool.
17:54 JCaesar btw, ist there a cli way to run a code_export?
18:14 andromeda-galaxy Jceaser: thanks for the info, I'll let you know if I get it working
18:14 JCaesar I think the reason for that was that it tried to build a lot of heaps of who knows what.
18:15 JCaesar Reminds me, adding an ebuild for the afp would also be nice… Oh foo.
18:15 int-e JCaesar: isafor defines a theory that contains a export_code command, and puts that into a session of its own.
18:16 JCaesar I have a theory with the command. I just want to run it.
18:16 int-e (which means it produces a useless heap image... but disk space is cheap)
18:17 JCaesar Hmpf. Maybe if I had remembered to put it into the root file…
18:17 int-e I don't think `isabelle build` can justn build a single theory file; one needs a ROOT file that defines a session that includes the theory.
18:18 int-e (but I'm not 100% sure)
18:21 ThreeOfEight pretty sure that's the case
18:21 ThreeOfEight andromeda-galaxy: Isabelle really isn't meant to be packaged
18:22 ThreeOfEight I think Makarius has some pretty strong opinions on this
18:22 JCaesar I wish I could say "I smell a hostile fork." more often…
18:23 ThreeOfEight but my guess would be that you'd have to do "isabelle build -b HOL" and then grab the heap files and put them in a tarball
18:23 ThreeOfEight or rather "isabelle build -s -b HOL" for a system-wide install (for which ISABELLE_HOME should be set)
18:23 ThreeOfEight then you can put the contents of ISABELLE_HOME into the tarball and that should contain everything
18:24 ThreeOfEight you might have to watch out for 32 Bit/64 Bit Poly-ML
18:25 ThreeOfEight the use of 64 Bit Poly-ML is discouraged, because it almost doubles memory usage and has no real advantage over 32 Bit Poly-ML except for really huge applications, which are very rare
18:26 int-e It's completely understandable too: Makarius doesn't want to waste time on debugging other packager's mistakes.
18:26 ThreeOfEight if the 32 bit libraries are not installed, Isabelle falls back on 64 bit, and if you ship the "wrong" kind of heap images, Isabelle will probably build the right ones upon startup
18:27 ThreeOfEight also, note that the HOL heap image is several hundred MiB, so I'm not quite sure you want to package that
18:27 ThreeOfEight even though it only takes about 5 minutes to build it
18:27 ThreeOfEight er, s/even though/especially since/"
18:32 ThreeOfEight int-e: one can also say quite reasonably that since Isabelle has roughly one release per year and they are not backwards-compatible at all, packaging Isabelle doesn't make that much sense
18:32 ThreeOfEight since automatic updates are a bad idea without backwards compatibility
18:33 ThreeOfEight so the only benefit of a package is that you can write "emerge isabelle2016" instead of downloading and untarring it yourself and make a few symlinks, which isn't a huge amount of effort
18:36 JCaesar ThreeOfEight: The benefit I see and want is that all the software I have installed is centrally managed.
23:00 andromeda-galaxy ThreeOfEight: sorry I missed you earlier, I understand the problems (also, thanks for the suggestion about using system-wide install)!  I agree with what JCaesar was saying, the rationale for packaging it is that it's centrally managed, easy to uninstall, and I have a uniform interface for managing everything

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary