Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-07-23

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

All times shown according to UTC.

Time Nick Message
00:00 deep-book-gk_ left #isabelle
01:13 __marioxcc joined #isabelle
01:13 __marioxcc Hello.
01:31 JCaesar __marioxcc: Just fyi: most people in this channel are in Germany. And it's 3:30 there right now.
01:32 JCaesar So you might wanna ask your question, stay, and see if you have an answer tomorrow.
01:32 JCaesar (Oh, and no, Proof General stopped working with Isabelle around 2014, iirc.)
01:37 __marioxcc JCaesar: Ok. Thanks. I assume you readed my question from around 24 hours ago.
01:37 __marioxcc So using jEdit/Isabelle is mandatory now?
01:38 JCaesar Yes.
01:38 __marioxcc Oh. :(
01:39 __marioxcc Too bad. I am looking for a more "interoperable" system (I.e.: I'm not tied to a particular editor).
01:39 JCaesar __marioxcc: we all are.
01:39 __marioxcc ?
01:40 __marioxcc Well, what would you suggest JCaesar? I don't recall if I mentioned that I'm new to proof assistants and I intend to develop a formalization of chemical nomenclature.
01:40 __marioxcc (what proof verifier/assitant)
01:42 __marioxcc Coq seems to be the most popular one, so I guess at least it has community size as a point on its favor. However, I am not interested in learning constructive logic.
01:50 JCaesar Let's just say that there are quite a few people in the Isabelle community that are not happy with the current editor situation. Then again, we all are aware how powerful the interactivity provided by the current jedit implementation is…
01:51 ilbot3 joined #isabelle
01:51 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/
02:00 __marioxcc Ok.
02:00 __marioxcc JCaesar: What happened to the Emacs mode? Did it stop working working or is it merely missing new features?
02:02 JCaesar I think at first it was only missing new features (Peter was still using it in 2013), but now it really doesn't work at all anymore.
02:03 __marioxcc I see. Thanks.
02:05 JCaesar and from what I've heard it's not so easy to just implement the interface for a new editor. I've also heard that there is something being worked on, but it's got nothing to do with emacs. It seems it's more of the electron-kind.
02:06 __marioxcc JCaesar: Sorry, what is Electron-kind?
02:07 JCaesar the thing that is chrome without being a browser? I don't know exactly either. But I think that atom-editor (the one that takes 13% of your cpu to blink its cursor) is implemented in it.
02:08 __marioxcc Ok.
02:08 __marioxcc I'm not at all interested in Google evil technologies, so I have zero idea about that.
02:09 JCaesar same here… i'd like a nice, leightweight ncurses-or-so window that displays the current output state of isabelle depending on whichever line your editor says the cursor is currently on. but that's not the world we live in.
02:12 __marioxcc Yes, but "somebody" can implement something like that.
02:14 JCaesar Sure. "some time". ;)
02:14 __marioxcc Haha.
02:15 JCaesar ammbauer: You wanted to do something like that, no? __marioxcc: You just gotta find a way to get him paid for that.
02:15 __marioxcc Glancing at HOL4 official tutorial, I get the impression that it has a somewhat usable in-REPL interface (at least it shows subgoals).
02:18 __marioxcc JCaesar: Hmm. Maybe I'd willing to pay for somebody to do that, but I hardly have any money to spare, and maybe there's already a proof assistant that has a feature like this.
02:19 JCaesar I don't know what you want to do with your proof assistant, anyway.
02:20 JCaesar hm, from what I remember, you can get jedit to behave reasonably similar to emacs, in terms of key combinations… maybe that is enough anyway.
02:20 __marioxcc JCaesar: I want to write a formalization of chemical notation and then prove sanity features for it, like that it is complete (assingns a name to every compound).
02:22 JCaesar hm, that does sound like constructive logic would not be a hindrance at all. But I guess you better ask someone who has a better overview. Maybe larsrh?
02:24 __marioxcc I don't really know because I do not know about constructive logic at all.
02:26 JCaesar well, essentially, you lose a few proof methods. Like proof by contradiction.
02:28 __marioxcc And I gain... nothing?
02:30 JCaesar You gain the fact that all your existentials are executable, i.e. if you know that ?x. P x then you can execute the proofs like a program and obtain an actual example of x.
02:30 JCaesar at least in theory. I don't know if Coq actually does that.
02:34 __marioxcc That does not seem interesting to me at all.
02:35 __marioxcc After all, in mathematics one is used to find a more or less repertorie of examples for {groups, topological spaces, vector spaces, etc...}
05:24 wagle joined #isabelle
10:13 silver joined #isabelle
10:28 ammbauer joined #isabelle
11:24 larsrh "Google evil technologies" like Chrome???
13:20 JCaesar Yeah, how could Google be evil, if even their motto is "don't be evil". (Don't ask me. I only wanted to agree on the fact that I'm not interested in electron.)
13:25 int-e I always thought that Google has been redefining "evil" since 2003.
13:26 int-e I missed this: 'When forming its parent company Alphabet last year, Google dropped its old motto, “Don't be evil,” and exchanged it with, “Do the right thing.”'
13:26 larsrh luckily with jEdit we rely on Oracle, who are definitely less evil than Google
13:27 int-e could you please say that again, slowly... I can't believe my ears... eyes... whatever ;-)
13:27 int-e The only way in which Oracle is less evil is that they're a smaller company.
13:27 larsrh </sarcasm>
13:28 larsrh unless you're only using GNU products I think you're going to have a hard time not using anything that has been touched by a large corporation
13:30 int-e I guess we've been expelled from paradise.
23:08 stoopkid_ joined #isabelle
23:15 juanbono joined #isabelle

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