Haudegen has quit [Remote host closed the connection]
zlsyx has quit [Read error: Connection reset by peer]
zlsyx has joined #ocaml
hdon has quit [Ping timeout: 260 seconds]
pierpa has joined #ocaml
infinity0_ has joined #ocaml
infinity0_ has quit [Changing host]
infinity0 is now known as Guest90128
infinity0_ has joined #ocaml
Guest90128 has quit [Killed (weber.freenode.net (Nickname regained by services))]
infinity0_ is now known as infinity0
pmetzger has quit [Ping timeout: 256 seconds]
<chindy>
I can run utop and then do #require "core";; open Core;; let _ = String.strip " akj kj" and it works perfectly. However When I have the same lines in an ocaml file and try to compile with ocamlbuild -pkg core Main.native I get the following error: Error: No implementations provided for the following modules:
<chindy>
Command exited with code 2.
<chindy>
Condition referenced from /home/julian/.opam/4.06.1/lib/core/core.cmxa(Core__Mutex0)
<chindy>
Mutex referenced from /home/julian/.opam/4.06.1/lib/core/core.cmxa(Core__Mutex0)
<chindy>
Hint: Recursive traversal of subdirectories was not enabled for this build,
<chindy>
Any ideas why that might be ?
al-damiri has quit [Quit: Connection closed for inactivity]
pmetzger has joined #ocaml
silver has quit [Read error: Connection reset by peer]
mfp has quit [Ping timeout: 240 seconds]
pmetzger has quit []
Duns_Scrotus is now known as ichigo_best_girl
FreeBirdLjj has joined #ocaml
hdon has joined #ocaml
zlsyx has quit [Remote host closed the connection]
hdon has quit [Ping timeout: 264 seconds]
tormen_ has joined #ocaml
<def`>
chindy: -tag thread
moei has quit [Read error: Connection reset by peer]
tormen has quit [Ping timeout: 260 seconds]
moei has joined #ocaml
<rgr[m]>
def`: take a look at my merlin.el pr's :)
FreeBirdLjj has quit [Ping timeout: 264 seconds]
shinnya has quit [Ping timeout: 263 seconds]
pierpa has quit [Quit: Page closed]
cobreadmonster has joined #ocaml
FreeBirdLjj has joined #ocaml
mk9 has joined #ocaml
mk9 has quit [Client Quit]
mk9 has joined #ocaml
pierpal has quit [Ping timeout: 240 seconds]
FreeBirdLjj has quit [Ping timeout: 248 seconds]
govg has joined #ocaml
pierpal has joined #ocaml
pierpal has quit [Client Quit]
pierpal has joined #ocaml
pierpal has quit [Read error: Connection reset by peer]
pierpal has joined #ocaml
FreeBirdLjj has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 256 seconds]
pierpal has quit [Read error: Connection reset by peer]
hdon has joined #ocaml
hdon has quit [Ping timeout: 256 seconds]
pierpal has joined #ocaml
cbot_ has joined #ocaml
cbot has quit [Ping timeout: 268 seconds]
FreeBirdLjj has joined #ocaml
ygrek has joined #ocaml
shinnya has joined #ocaml
pierpal has quit [Read error: Connection reset by peer]
jimmyrcom_ has joined #ocaml
muelleme has joined #ocaml
pierpal has joined #ocaml
mk9 has quit [Quit: mk9]
muelleme has quit [Ping timeout: 265 seconds]
cobreadmonster has quit [Quit: Connection closed for inactivity]
cbot_ has quit [Quit: Leaving]
pierpal has quit [Read error: Connection reset by peer]
FreeBirdLjj has quit [Ping timeout: 265 seconds]
FreeBirdLjj has joined #ocaml
muelleme has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 248 seconds]
pierpal has joined #ocaml
zolk3ri has joined #ocaml
FreeBirdLjj has joined #ocaml
pierpal has quit [Read error: Connection reset by peer]
pierpal has joined #ocaml
bartholin has joined #ocaml
pierpal has quit [Ping timeout: 248 seconds]
<bartholin>
What is a ppx? Where is the documentation? Where are the tutorials?
<kit_ty_kate>
This module is the included in the Containers module so everything is available by default if you use « open Containers »
tarptaeya has quit [Quit: Konversation terminated!]
pierpal has joined #ocaml
<kit_ty_kate>
-the
<silenc3r>
by the way, which style is preferred when using Containers: using open Containers or CC-functions?
hdon has joined #ocaml
hdon has quit [Ping timeout: 240 seconds]
<Gurkenglas>
opam 2.0's opam install coq fails at camlp5.7.05 with "../tools/ocamlopt.sh: Zeile 5: ocamlopt: Kommando nicht gefunden." (~"Command not found.")
<Gurkenglas>
(Zeile -> Line)
<kit_ty_kate>
silenc3r: open Containers if you can, I guess
pierpal has quit [Read error: Connection reset by peer]
<kit_ty_kate>
you can even use the -open option if you are tired of adding opens to every modules
zlsyx has quit [Remote host closed the connection]
tarptaeya has joined #ocaml
mk9 has joined #ocaml
<chindy>
def`: that did not work
tarptaeya has quit [Quit: Konversation terminated!]
pierpal has joined #ocaml
zlsyx has joined #ocaml
jmiven has quit [Quit: co'o]
jmiven has joined #ocaml
pierpal has quit [Remote host closed the connection]
gtrak has joined #ocaml
<Gurkenglas>
My Ocaml's bin does not have an ocamlopt file. Why, and how do I fix this?
gtrak has quit [Ping timeout: 260 seconds]
JeanMax has joined #ocaml
gtrak has joined #ocaml
<flux>
gurkenglas, make world.opt
<flux>
(I'm assuming you self-compiled your ocaml)
<flux>
btw, it may also be called ocamlopt.opt
JeanMax has quit [Read error: Connection reset by peer]
sh0t has joined #ocaml
shinnya has quit [Ping timeout: 240 seconds]
muelleme has quit [Ping timeout: 260 seconds]
<Gurkenglas>
Did that, still no ocamlopt
<Gurkenglas>
*flux
<Gurkenglas>
(maybe a problem with multiple bins and targeted locations and where PATH points?)
<flux[m]>
do you run an exotic platform that might not support native compilation?
mk9 has quit [Quit: mk9]
troydm has quit [Ping timeout: 264 seconds]
muelleme has joined #ocaml
pierpal has joined #ocaml
muelleme has quit [Ping timeout: 265 seconds]
FreeBirdLjj has quit [Remote host closed the connection]
andreypopp has joined #ocaml
andreypopp has quit [Remote host closed the connection]
markhkim has joined #ocaml
gareppa has joined #ocaml
pmetzger has joined #ocaml
FreeBirdLjj has joined #ocaml
pierpal has quit [Ping timeout: 240 seconds]
pierpal has joined #ocaml
pierpal has quit [Ping timeout: 256 seconds]
gtrak has quit [Ping timeout: 276 seconds]
GreyFaceNoSpace has joined #ocaml
gtrak has joined #ocaml
gareppa has quit [Quit: Leaving]
troydm has joined #ocaml
<Gurkenglas>
flux[m], what command shows what platform I'm currently ssh'd onto?
domanic has joined #ocaml
<Gurkenglas>
flux[m], I am able to use the opam command after compiling
<companion_cube>
silenc3r: I use CC-functions, but it seems most people open containers :D
<Gurkenglas>
ocamlc even
<pmetzger>
Gurkenglas: you mean like hostname and uname?
<pmetzger>
("platform" is the host name? the operating system version?)
<Gurkenglas>
pmetzger, no, platform in the sense of "exotic platform that might not suppoer native compilation" flux[m] said
<pmetzger>
I don't understand what you mean. (I've also only been on since the top of the hour, so I don't have scrollback more than 36 minutes or so.)
<Gurkenglas>
Should that also contain a file called ocamlopt?
<Gurkenglas>
If so, what happened?
<pmetzger>
no idea. I didn't build this for you. :)
<pmetzger>
but if the question is what the _architecture_ is (that's clearly what was meant), do uname -a and see what the architecture is. It is 99.9% likely not anything exotic.
<Gurkenglas>
flux[m], I think the relevant part is "GNU/Linux"
<pmetzger>
No.
<pmetzger>
That's not the architecture.
<pmetzger>
The architecture is what sort of processor you're running on. Paste the output of uname -a
<Gurkenglas>
I think that output contains identifying information
<pmetzger>
What do you mean, contains identifying information?
<pmetzger>
It tells us the OS, the hardware type, etc.
<Gurkenglas>
Contains the server name, at least
<pmetzger>
Yah, so what?
<octachron>
Gurkenglas, is "uname -a | grep x86" empty?
gareppa has joined #ocaml
<Gurkenglas>
not empty
<pmetzger>
So you're running on an x86 and nothing is exotic.
<octachron>
then you are on a standard architecture and did not build ocamlopt before doing make install
<flux[m]>
Gurkenglas: which steps did you take to install ocaml?
<mrvn>
Gurkenglas: you probably shouldn't compile ocaml yourself but simply install the precompiled packages for your distribution.
<pmetzger>
You've been struggling to get this working for over 24 hours. Maybe it's time to just build a VM for yourself on your windows box, install Ubuntu or Debian or what have you, and add the package. You will be done in an hour instead.
<Gurkenglas>
mrvn, I don't have root
<pmetzger>
mrvn: He can't, he doesn't have root on some machine at his school.
<pmetzger>
mrvn: He should probably just build a VM locally on his Windows machine with Virtual Box.
<mrvn>
Gurkenglas: even better. That means you have someone to do this for you.
<Gurkenglas>
pmetzger, it took me longer to get stuff done when I did things on VMs
<Gurkenglas>
mrvn, they wouldn't even install a Haskell compiler
<pmetzger>
Gurkenglas: Longer than fighting for a day to do something you don't really understand how to do for yourself? You clearly don't have a long background doing Unix sysadmin tasks. It will take an hour to set up a VM and then you'll be done.
<pmetzger>
I'm not trying to denigrate your skills, I'm just trying to be pragmatic.
<pmetzger>
The fast way to do this is just to have root on some machine and install the packages.
<Gurkenglas>
It's years back, but I think it took on the order of half a day to a few days to set up a VM the last time I tried, and then came the installation problems
<pmetzger>
For me, I could build and install for myself in a few minutes but I've been doing Unix sysadmin for decades.
<pmetzger>
"A few days"?
<pmetzger>
What?
<pmetzger>
What?
<Gurkenglas>
Downloading the virtualbox software, finding the right distribution
<pmetzger>
Start virtualbox on an ubuntu install CD and it will be in place in a few minutes. Then use the GUI package manager to just install everything.
<pmetzger>
You can get an install CD in five minutes if you have a decent internet connection.
<pmetzger>
I'm just suggesting that since you're not comfortable reading makefiles, reading shell scripts, etc., that you're not in a position to debug this
<pmetzger>
you were even paranoid about pasting uname -a which is harmless.
<pmetzger>
Given this, don't try to build this on your own. Either rent a VM for $5 a month or set one up on your machine.
<pmetzger>
Then you can just do "apt-get install ocaml opam coq" as root and be done.
<pmetzger>
You've been trying the hard way for over a day after all,
<Gurkenglas>
I just used the uname -a output and information and google to get information that I think I could use to identify me
<Gurkenglas>
I've installed Coq on Windows, but CoqHammer doesn't work on Windows
iZsh has quit [Ping timeout: 268 seconds]
<pmetzger>
That has instructions for installing a VM running Linux. Click on the link.
<Gurkenglas>
By CD, do you mean that I would need a CD burner?
<pmetzger>
NO.
<pmetzger>
You download a CD image and you point virtualbox at the image. It mounts a virtual CD into the virtual CD drive from the image and boots it.
<Gurkenglas>
Sure, I'll try the instructions in that link
<Gurkenglas>
Let's see if I can free up 4 gigs of space without windows update pouncing on the chance
<pmetzger>
I think you might need to get a technically adept friend who has done things like setting up VMs to work with you in person, sitting next to you on your machine, to help you. It will speed things up a lot.
<pmetzger>
like the difference between this taking less than an hour and several more days of agony for you.
<pmetzger>
If you don't even have 4G free on your machine setting up a VM will be painful.
iZsh has joined #ocaml
<Gurkenglas>
Hah, I'm the technically adept friend around here
<Gurkenglas>
Perhaps the virtual box should be installed on the server where the builds fail?
<pmetzger>
Why don't you just google for virtual box?
<pmetzger>
You will need a more technically adept person to help I suspect.
<Gurkenglas>
I can download VirtualBox, I was just reporting a bug in that help file
<Gurkenglas>
I suppose I can post an issue instead, or edit the wiki
<pmetzger>
If you want to report a bug, tell the Coq people, I'm not able to fix it.
muelleme has joined #ocaml
<pmetzger>
Yes, post an issue, or edit the wiki, or both.
<steenuil>
the instructions look clear enough to me, maybe the wiki just doesn't need a VirtualBox page?
<pmetzger>
Normally I prefer to have 20G free per VM I set up. If your hard drive is almost full you'll have a lot of trouble.
spectrumgomas[m] has joined #ocaml
Gurkenglas_ has joined #ocaml
andrewalker has joined #ocaml
muelleme has quit [Ping timeout: 264 seconds]
<pmetzger>
If I recall correctly, right now if you download virtualbox for windows you need to get one rev back because they haven't yet released the windows build of the last release (which was a few days ago.)
Gurkenglas has quit [Ping timeout: 256 seconds]
<pmetzger>
Once you have Ubuntu installed, you can also use a GUI package manager like Synaptic to install packages for you without having to deal with the command line.
moolc has joined #ocaml
<pmetzger>
You may find, btw, that installing Coqhammer is difficult even given that you have your own VM, but it will be simpler than trying to do it on a machine you don't control.
Ulrar has joined #ocaml
cbarrett has joined #ocaml
ichigo_best_girl has joined #ocaml
M-martinklepsch has joined #ocaml
ilovezfs_ has joined #ocaml
multiocracy[m] has joined #ocaml
isaachodes[m] has joined #ocaml
FreeBirdLjj has quit [Read error: Connection reset by peer]
FreeBirdLjj has joined #ocaml
isaachodes[m] has quit [Ping timeout: 256 seconds]
multiocracy[m] has quit [Ping timeout: 256 seconds]
M-martinklepsch has quit [Ping timeout: 256 seconds]
spectrumgomas[m] has quit [Ping timeout: 246 seconds]
bli[m] has quit [Ping timeout: 246 seconds]
smondet[m] has quit [Ping timeout: 246 seconds]
orbifx[m] has quit [Ping timeout: 246 seconds]
Haudegen[m] has quit [Ping timeout: 246 seconds]
caseypme[m] has quit [Ping timeout: 240 seconds]
drsmkl[m] has quit [Ping timeout: 240 seconds]
olopierpa[m] has quit [Ping timeout: 255 seconds]
yetanotherion[m] has quit [Ping timeout: 255 seconds]
M-jimt has quit [Ping timeout: 255 seconds]
talyian[m] has quit [Ping timeout: 255 seconds]
tiksin[m] has quit [Ping timeout: 240 seconds]
remix2000[m] has quit [Ping timeout: 240 seconds]
mmmmmmmmmmmm[m] has quit [Ping timeout: 245 seconds]
flux[m] has quit [Ping timeout: 245 seconds]
dlebrecht[m] has quit [Ping timeout: 245 seconds]
aantron has quit [Ping timeout: 245 seconds]
equalunique[m] has quit [Ping timeout: 260 seconds]
regnat[m] has quit [Ping timeout: 260 seconds]
srenatus has quit [Ping timeout: 260 seconds]
ansiwen has quit [Ping timeout: 260 seconds]
loxs[m] has quit [Ping timeout: 276 seconds]
peddie[m] has quit [Ping timeout: 276 seconds]
rgr[m] has quit [Ping timeout: 276 seconds]
aspiwack[m] has quit [Ping timeout: 276 seconds]
hcarty[m] has quit [Ping timeout: 256 seconds]
Bluddy[m] has quit [Ping timeout: 276 seconds]
copy` has quit [Ping timeout: 276 seconds]
hdurer[m] has quit [Ping timeout: 265 seconds]
FreeBirdLjj has quit [Remote host closed the connection]
jnavila has joined #ocaml
zlsyx has quit [Quit: Leaving...]
<bartholin>
how do I make the toplevel accept the command open Ast_mapper?
<pmetzger>
bartholin: what have you tried doing and what is the error you get?
domanic has quit [Quit: Konversation terminated!]
domanic has joined #ocaml
<bartholin>
pmetzger: I typed the command on the toplevel, and I got Error: Unbound module Ast_mapper I believe I should add something like #load "something.cma"
<steenuil>
bartholin: #require "compiler-libs";;
<pmetzger>
This is going to seem like a stupid topic, but: I've been using OCaml for the last six months or so and I have yet to really want to use the top level for much. Do people really use it extensively for things?
<bartholin>
Unknown directive `require'.
<steenuil>
are you not using utop?
<pmetzger>
Maybe "what do people use the top level for" would be an interesting question for discourse.ocaml.org....
<steenuil>
it's probably useful if you use something like emacs and can send things to it to evaluate on the fly
<bartholin>
steenuil: no, I am using ocaml...
<steenuil>
other than that, I use it for quickly testing something every once in a while
<steenuil>
bartholin: it works with ocaml too for me, maybe you need to install findlib?
domanic has quit [Ping timeout: 260 seconds]
<bartholin>
how
<bartholin>
I have ocamlfind
<pmetzger>
utop seems like it works much more nicely than the built in top level. "opam install utop"...
<steenuil>
I don't really know to be honest, I just install everything via opam and it works
<Gurkenglas_>
Was working on the ssh'd server again for lack of local hard drive space. (Also it's nice when you can continue work via ssh from your smartphone.) There was an ocamlopt file in the folder with the ocaml sources so I added that folder to the path and now opam install coq gets further, I think: http://lpaste.net/3960125709959036928
<Gurkenglas_>
Welp, the "this filesystem" link is dead x)
<pmetzger>
Gurkenglas_: Using user mode linux for this is madness.
muelleme has joined #ocaml
hdon has joined #ocaml
tane has joined #ocaml
govg has quit [Ping timeout: 248 seconds]
hdon has quit [Changing host]
hdon has joined #ocaml
govg has joined #ocaml
govg has quit [Ping timeout: 246 seconds]
Gurkenglas_ is now known as Gurkenglas
<pmetzger>
Honestly, this whole exercise sounds like masochism.
gtrak has quit [Ping timeout: 256 seconds]
<pmetzger>
I think you would be much happier if you had help from someone who is there with you and has experience doing this sort of thing.
<octachron>
pmetzger, could you tone a bit the hostility of your tone?
<pmetzger>
I'm not being hostile.
<pmetzger>
Really. It's not intended as hostile. It's intended as pragmatic.
<octachron>
You may disagree with the path chosen by Gurkenglas , but it is his choice to make
<pmetzger>
Of course.
<octachron>
and your repeated use of madness, masochism does sound quite strongly worded to me
<pmetzger>
But I think he's going to spend a lot of time only to not get to what he wants, which is a functioning Coq installation along with CoqIDE and CoqHammer.
<pmetzger>
I tend to use colorful language.
jimmyrcom_ has joined #ocaml
<octachron>
Isn't there a lot of things to learn on this path?
<pmetzger>
I don't even know how he'll run CoqIDE successfully over the network and you really can't use Coq at the command line successfully.
<pmetzger>
He might learn a lot, yes, but not about Coq or OCaml. :)
<octachron>
this is good point, running graphical interface over ssh can be too slow to be useful
<pmetzger>
But my goal is to get him to what he wants cleanly and with minimal fuss. I'm not trying to be hostile. Unfortunately tone is hard to read over the network.
<Gurkenglas>
pmetzger's language is fine, I ~grew up on 4chan :P
<Gurkenglas>
I'm using ProofGeneral on emacs for the ide part, no need for graphics
<pmetzger>
ProofGeneral works much better with a local emacs. Otherwise you don't get most of the really important features.
<pmetzger>
Well, you don't get *many* important features.
<pmetzger>
Local GUI emacs vs. terminal emacs.
<pmetzger>
You can do it but it won't be fun.
<steenuil>
can't you connect it to a remote coq repl?
<flux>
GUI Emacs works over network as well..
<Gurkenglas>
I plan to have Coq and ProofGeneral and Emacs on the machine I'm connecting to with ssh
<Gurkenglas>
(using the emacs part already)
<pmetzger>
Yes, but you won't have the GUI emacs running locally. If you can remote display back Emacs then you're okay, but you don't have an X server running locally so I don't think that will work even if you were willing to put up with the slow performance.
<pmetzger>
steenuil might be right that you might be able to convince a local Emacs to connect to a remote coq REPL but I don't know if that will work correctly.
<pmetzger>
(I don't know if Proof General has to send signals to the coq process etc.)
<pmetzger>
This is a lot of work to make something work badly.
<pmetzger>
What's the real problem with running a VM on your Windows box?
<steenuil>
I thought you could just connect it to any repl like in common lisp
<pmetzger>
steenuil I don't understand enough about the innards of ProofGeneral. I've deliberately avoided learning.
<pmetzger>
And there's now some advanced protocol between ProofGeneral and the Coq command line that makes it even more fun.
<Gurkenglas>
What example feature of ProofGeneral would this miss?
<pmetzger>
Gurkenglas: Yes, I know you can run Emacs inside a terminal. The problem is then you can't do Unicode, can't get partial coloring of the proven area to tell you it is immutable, etc. etc. etc.
<pmetzger>
That's running inside a terminal. Which is different from the capabilities of Emacs when it has direct access to the display server and controls its own window.
<pmetzger>
It can't even handle all the same keystrokes because many key combinations aren't available in ASCII
<pmetzger>
Anyway, what's the problem with running a VM again?
<pmetzger>
If you have too many movies or something on the local hard drive, you can pick up a big thumb drive at your corner pharmacy for the price of a package of cigarettes.
<pmetzger>
(and for much less than a bottle of booze.)
<moolc>
Gurkenglas: what font is that?
<Gurkenglas>
moolc, I don't know, I just copypasted the symbol from somewhere
<pmetzger>
It's whatever font he has in his SSH client.
<moolc>
Gurkenglas: i mean the default emacs font
<pmetzger>
he's using a terminal connection over ssh. it's whatever his client has.
<pmetzger>
I mean, get a raspberry pi if you need to. $35.
<pmetzger>
It's less pain than all this.
webshinra has joined #ocaml
<Gurkenglas>
moolc, "describe-font" says "no fonts being used"
<pmetzger>
Though Coqhammer isn't going to run well without a really powerful machine behind it. And IIRC it isn't stable.
<pmetzger>
Of course it says no fonts are in use, it is running in the terminal, not in the GUI!
<Gurkenglas>
pmetzger, I chose to do it on the remote side because of space and being able to use it from, say, my smartphone
<pmetzger>
Emacs has no knowledge of what's on the other side, it's just sending terminal escape codes.
<pmetzger>
You can't use Coq reasonably from your smartphone in ProofGeneral. Running emacs in a smartphone is going to be very very painful.
<pmetzger>
Never mind.
<pmetzger>
Look, I've used Coq _a lot_. This is my advice. You don't have to listen to it, but you know what it is.
<Gurkenglas>
(In case that's not what you meant by "Never mind.", the smartphone would only run an ssh client onto that same remote server)
<pmetzger>
Have you used Emacs long?
<Gurkenglas>
Intermittently for a year, perhaps?
<pmetzger>
In particular, have you tried to really use emacs over ssh on a smart phone? That's more than I would have patience for.
<Gurkenglas>
It's a bit annoying to get a ctrl key
<pmetzger>
And how will you send any proof general commands without the control key and the meta key?
mk9 has joined #ocaml
<Gurkenglas>
Using alternative keyboards
<pmetzger>
You've used proof general and coq for long?
<Gurkenglas>
I've not used proof general, I've used Coq for a few weeks
<companion_cube>
on a tablet I suppose coq could run
<companion_cube>
but the UI might not be that great :D
<pmetzger>
companion_cube: coqhammer will not make him friends with the other users of the machine at his university. It's very very CPU intensive. Assuming he gets it working.
<companion_cube>
yeah, I guess
hdon has quit [Ping timeout: 246 seconds]
<companion_cube>
it sounds like coqhammer could provide a docker image, or something, if it's that hard to install
<pmetzger>
Anyway, chacun a son goût. Good luck, Gurkenglas.
<pmetzger>
companion_cube: It isn't that hard to install, but it's research code, and he's having trouble installing ocaml itself.
<pmetzger>
Coqhammer is like the Hammer stuff for Isabelle/HOL. It sends off a fleet of processes trying different proof search strategies. It uses SMT solvers, neural nets, everything anyone was ever able to think of.
<pmetzger>
Eats your computer, but if you're trying to build a big formally verified system it's nicer than trying to do the proofs by hand.
<companion_cube>
I mean you also need to install cvc4, etc. I suppose, right?