EvanR 2017-02-18 13:45:39
if hypothetically the program does halt, it stands as a proof of termination, just run it and see
EvanR 2017-02-18 13:45:39
since this is supposed to get a contradiction, that doesnt work!
dolio 2017-02-18 13:46:58
No.
dolio 2017-02-18 13:47:10
The execution trace would be a proof of termination, maybe.
ezyang 2017-02-18 13:47:27
One has to be careful about the modality of these types of statements
dolio 2017-02-18 13:49:46
Unless the program is written in some system where all programs terminate. Then I'd accept it as a proof of termination.
EvanR 2017-02-18 13:51:25
and if you are evaluating under a binder that introduces a false hypothesis aiming for a contradiction, i can see that blowing up in your face
dolio 2017-02-18 13:53:06
Yes, you have to be careful. There are systems where normalizing in a consistent context must terminate, but may fail to terminate in an inconsistent context.
Prutheus 2017-02-18 13:53:43
jaspe/quit
EvanR 2017-02-18 13:55:05
ok, marking that off my list of assertions which dont seem completely convincing
maksim__ 2017-02-18 14:14:54
i'm trying debug a program and for the life of me i can't figure out where this exception is coming from
maksim__ 2017-02-18 14:14:57
solr: createProcess: runInteractiveProcess: exec: does not exist (No such file or directory)
maksim__ 2017-02-18 14:15:25
i've tried so many different things but i'm kind of at my wit's end
maksim__ 2017-02-18 14:15:58
the symbol runInteractiveProcess doesn't appear in my codebase
maksim__ 2017-02-18 14:16:02
but createProcess does
maksim__ 2017-02-18 14:16:32
some advice
maksim__ 2017-02-18 14:18:52
it's saying solr doesn't exist
hpc 2017-02-18 14:21:17
what happens if you run "which solr"?
maksim__ 2017-02-18 14:21:28
i don't have solr
maksim__ 2017-02-18 14:21:35
i'm trying to get this thing to talk to solr over http
hpc 2017-02-18 14:22:11
ah
hpc 2017-02-18 14:22:23
it looks like what your code may actually be doing is attempting to launch solr itself
maksim__ 2017-02-18 14:22:36
can you show me where exactly that happens
maksim__ 2017-02-18 14:22:37
http://pastebin.com/McfAZ5hn
maksim__ 2017-02-18 14:23:37
this is the definition of ?$>
maksim__ 2017-02-18 14:23:38
http://pastebin.com/RsVtmXgp
maksim__ 2017-02-18 14:24:08
which i don't quite understand
hpc 2017-02-18 14:24:34
that whole thing is just running solr
hpc 2017-02-18 14:24:53
if you want to talk to it over http, you need an http library or something
maksim__ 2017-02-18 14:25:06
yes i understand that much but i want it to fail gracefully
maksim__ 2017-02-18 14:25:11
instead of throwing an exception
maksim__ 2017-02-18 14:25:27
where does the actual call to run happen?
hpc 2017-02-18 14:25:35
createProcess
hpc 2017-02-18 14:25:48
cr defines what process to run, then createProcess does the thing
maksim__ 2017-02-18 14:26:05
yes
maksim__ 2017-02-18 14:26:46
i think this line is supposed to being the graceful fail
maksim__ 2017-02-18 14:26:48
p <- fromMaybe fg (conf C.! "run") ?$> Proc.createProcess cr
maksim__ 2017-02-18 14:27:03
`conf C.! "run"` just gets the run key from conf
maksim__ 2017-02-18 14:27:11
*run value
hpc 2017-02-18 14:27:53
sort of
hpc 2017-02-18 14:28:11
it tests a boolean value and decides if it should do something or produce an "empty" value
hpc 2017-02-18 14:28:27
since you want to handle an exception, the way to do that is to catch the exception
maksim__ 2017-02-18 14:28:58
what is it here?
hpc 2017-02-18 14:28:59
which i believe there is something that'll translate exceptions to Either somewhere in base
maksim__ 2017-02-18 14:29:07
the operator ?$> ?
hpc 2017-02-18 14:29:22
yeah
maksim__ 2017-02-18 14:29:55
what does the `pure` keyword mean?
benzrf 2017-02-18 14:30:20
maksim__: it's not a keyword - just a normal function. it's a method in the Applicative class
maksim__ 2017-02-18 14:30:37
so map pure over the functor f
maksim__ 2017-02-18 14:30:38
right?
hpc 2017-02-18 14:32:43
there's actually two different uses of pure there
hpc 2017-02-18 14:32:49
the first one is for m, the second is for f
maksim__ 2017-02-18 14:36:38
well okay i figured out how to make it not exception
maksim__ 2017-02-18 14:37:14
by putting run = "false" in the config
