divyanshu has quit [Quit: Computer has gone to sleep.]
boogie has quit [Remote host closed the connection]
jao has joined #ocaml
jao has quit [Changing host]
jao has joined #ocaml
jwatzman|work has quit [Quit: jwatzman|work]
eikke__ has quit [Ping timeout: 258 seconds]
racycle has quit [Quit: ZZZzzz…]
q66 has quit [Quit: Leaving]
divyanshu has joined #ocaml
ontologiae has quit [Ping timeout: 240 seconds]
oriba has joined #ocaml
oriba has quit [Client Quit]
divyanshu has quit [Quit: Computer has gone to sleep.]
ousado has quit [Remote host closed the connection]
ousado has joined #ocaml
cross has joined #ocaml
maattdd has quit [Ping timeout: 265 seconds]
claudiuc has quit [Remote host closed the connection]
manizzle has quit [Ping timeout: 240 seconds]
studybot_ has quit [Read error: Connection reset by peer]
BitPuffin has quit [Ping timeout: 240 seconds]
shinnya has quit [Ping timeout: 258 seconds]
BitPuffin has joined #ocaml
studybot has joined #ocaml
malo has quit [Quit: Leaving]
BitPuffin has quit [Ping timeout: 265 seconds]
BitPuffin has joined #ocaml
lopex has quit [Ping timeout: 245 seconds]
puzza007 has quit [Ping timeout: 245 seconds]
divyanshu has joined #ocaml
lopex has joined #ocaml
puzza007____ has joined #ocaml
jao has quit [Remote host closed the connection]
BitPuffin has quit [Ping timeout: 240 seconds]
john3213 has joined #ocaml
john3213 has left #ocaml [#ocaml]
jao has joined #ocaml
jao has quit [Changing host]
jao has joined #ocaml
racycle has joined #ocaml
araujo has quit [Quit: Leaving]
BitPuffin has joined #ocaml
johnf has quit [Ping timeout: 240 seconds]
jao has quit [Ping timeout: 240 seconds]
axiles has joined #ocaml
racycle has quit [Quit: ZZZzzz…]
divyanshu has quit [Quit: Computer has gone to sleep.]
divyanshu has joined #ocaml
claudiuc has joined #ocaml
ygrek_ has joined #ocaml
siddharthv_away is now known as siddharthv
ygrek_ has quit [Ping timeout: 245 seconds]
zpe has joined #ocaml
rgrinberg has quit [Quit: Leaving.]
ygrek_ has joined #ocaml
studybot_ has joined #ocaml
studybot has quit [Ping timeout: 245 seconds]
ygrek_ has quit [Ping timeout: 276 seconds]
ebzzry has quit []
ebzzry has joined #ocaml
studybot_ has quit [Quit: where is the love...]
studybot has joined #ocaml
studybot is now known as hacker
hacker is now known as studybot
ggole has joined #ocaml
zpe has quit [Remote host closed the connection]
Simn has joined #ocaml
adrien_oww has quit [Ping timeout: 276 seconds]
adrien_oww has joined #ocaml
ygrek_ has joined #ocaml
zpe has joined #ocaml
eikke__ has joined #ocaml
ebzzry has quit [Remote host closed the connection]
Kakadu has joined #ocaml
remyzorg has joined #ocaml
arj has joined #ocaml
gal_bolle has joined #ocaml
manizzle has joined #ocaml
avsm has joined #ocaml
nojb has joined #ocaml
manizzle has quit [Ping timeout: 252 seconds]
ontologiae has joined #ocaml
ikaros has joined #ocaml
ggole has quit [Ping timeout: 276 seconds]
ggole has joined #ocaml
ontologiae has quit [Ping timeout: 252 seconds]
Eyyub has joined #ocaml
rand000 has joined #ocaml
<Kakadu>
A little bit offtop
<Kakadu>
Let's we have a diagram which describes program (i.e. control flow graph)
<Kakadu>
there are some loops, ifs, setting variables' values
<Kakadu>
Importatnt: there is fork construction
<Kakadu>
Have you ever seem (not very big languages or something) which generate some useful code from these kind of diagrams?
<Kakadu>
seen*
<companion_cube>
most compilers use control flow graphs at some point
<companion_cube>
to determine variable lifetimes, for instance
<Kakadu>
I need something related two threads
<Kakadu>
too*
* Kakadu
spells everything wrong today
<companion_cube>
ah, forking...
<Kakadu>
I'm thinking how my input graphs will look like and it seems that map/reduce is not general case
<def`>
the fork spawns two processes that doesn't share address space?
<def`>
don't*
<gasche>
there has been some work on skeleton-based program parallelization that would be relevant
<def`>
rah, the fork spawns a second process not sharing the address space of its parent*
<Kakadu>
def`: It can share and can not. It seems that it will going to be some backends where threads are easy to be created (qtscript) and some backends where we need to evaluate at compile time how many threads (a.k.a. tasks) we will have and declare them in source files explicitly
<gasche>
I think SCADE is an example of industrial system where you program at a graphical dataflow level
<def`>
Kakadu: I remember encoding similar control flows using Arrows DSL in Haskell. I can't tell you how exactly this relate to your task though
<gasche>
I'm not sure it explicitly lets you talk about parallelism, though
<whitequark>
note that: "A symbol with internal or private linkage must have default visibility."
Kakadu has quit [Ping timeout: 240 seconds]
<jpdeplaix>
whitequark: ok, thanks. So I guess internal linkage is what I need
<whitequark>
yes
arjunguha has joined #ocaml
tobiasBora has quit [Quit: Konversation terminated!]
siddharthv is now known as siddharthv_away
ebzzry has joined #ocaml
Kakadu has joined #ocaml
eikke__ has joined #ocaml
avsm has quit [Quit: Leaving.]
ddosia has quit [Remote host closed the connection]
<Kakadu>
Btw, what is status of exceptions which are going to be declared in function body and not going to run out of scope of this function? Are they implemented?
eizo has joined #ocaml
<whitequark>
no
<whitequark>
the issue just got abandoned, and according to gasche maintainers are opposed to this
<flux>
that would be a new fature? defining exceptions without an internal module?
<flux>
let exception E = .. ?
<flux>
if it is implemented, then let type =.. should follwo :)
<flux>
and let class etc..
<flux>
actually I might quite like it!
maattdd has quit [Ping timeout: 245 seconds]
<whitequark>
flux: no, it was basically scoped goto
<whitequark>
exposing Pstatic_raise to the user
demonimin has quit [Ping timeout: 265 seconds]
<whitequark>
without any changes to the backend, what you want can be done by defining a local module
arjunguha has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
siddharthv_away is now known as siddharthv
_andre has joined #ocaml
arjunguha has joined #ocaml
claudiuc has joined #ocaml
avsm has joined #ocaml
<eikke__>
avsm: you're getting quite some praise in a /r/haskell discussion (about HalVM, and Mirage popped up)
ygrek_ has quit [Ping timeout: 258 seconds]
Thooms has quit [Ping timeout: 265 seconds]
Fullma has quit [Ping timeout: 258 seconds]
<gasche>
whitequark: note that optimizing local exceptions that do follow a no-escape (and no-lambda-crossing) restriction into static raise would certainly be a welcome optimization
<gasche>
(I would like "let <structure-item> in ..." to be valid in the general case, and "let exception ..." in particular, but I'm not sure we have the momentum to get that in if it's not compellingly optimized)
<avsm>
eikke__: heh, just independently replied to that thread
<gasche>
Pierre's branch would be a natural framework in which to do such an analysis, but it's probably doable at the lambda-level today already
thomassa has quit [Remote host closed the connection]
<avsm>
eikke__: sometimes the haskell community feels like it expects a tiny number of people to do all the work (cf the ICFP 2013 panel)
<gasche>
"Anil is a juggernaut of never-ending energy"
<gasche>
this is not praise, this is fact
<eikke__>
avsm: I wasnt at ICFP :(
siddharthv is now known as siddharthv_away
maattdd has joined #ocaml
* avsm
has just come back from visiting the home of OPAM in Nice and is feeling quite psyched. But now I'm looking at the opam 4.02 bulk build logs and feeling less happy :-)
<whitequark>
Drup: ping
<gasche>
don't tell us about that :-\
<Drup>
whitequark: pong
<whitequark>
I'm kind of unhappy with how the ppx support in ocamlfind combines with OASIS
<whitequark>
or better said, it's horrible
<Drup>
well, there is no support in oasis.
<gasche>
in the french complex and elitist bachelor system, some people have a lot of oral exams throughout the years to prepare for contests at the end of the year
<companion_cube>
o/ gasche
<whitequark>
so the ppx support in ocamlfind, which I've almost finished implementing, basically means that for e.g. ppx_tools, you'd have this
<gasche>
a well-known trick used by oral examiners is to start giving crappy notes, improve progressively and say at the end
<gasche>
"see, thanks to us you did a lot of progress"
<Drup>
the Require field for the META, as generated by oasis, is just a copy of BuildDepends, but you don't want the syntax packages in it most of the tim
<Drup>
so you need this XMETARequire
<Drup>
which is ... not intuitive.
<whitequark>
right.
<whitequark>
I think that should be something like
<whitequark>
BuildDepends: split into BuildDepends: and Depends:
<Drup>
probably
<Drup>
in practice, though
<Drup>
you want to depends on all the regular packages
<Drup>
and don't depend on the syntax extensions
<whitequark>
yes
<Drup>
so splitting into "BuildDepends" and "Syntax" would be good enough.
<whitequark>
yes
fraggle_ has joined #ocaml
<Drup>
I'm not sure which one of the two option is better, concerning ppx and options
<whitequark>
-package one, obviously, because it's compatible right now
<whitequark>
and works the same way as for camlp4 exts
<Drup>
right
<Drup>
whitequark: imho, post an email in the mailing list wg-camlp4 (and copy to gerd, I'm not sure he's following this one)
<Drup>
I'm sure alain frisch as a good idea on the question.
<Drup>
has*
arjunguha has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
<whitequark>
ok
<Drup>
(maybe copy gildor too)
jbrown has joined #ocaml
arjunguha has joined #ocaml
Kakadu has quit [Ping timeout: 240 seconds]
<whitequark>
hm, also need topfind support
maattdd has quit [Ping timeout: 258 seconds]
Thooms has quit [Quit: WeeChat 0.3.8]
Thooms has joined #ocaml
studybot has quit [Remote host closed the connection]
<ggole>
Sigh, having to short circuit by raising an exception makes me sad
ontologiae has joined #ocaml
ygrek_ has joined #ocaml
arjunguh_ has joined #ocaml
arjunguha has quit [Ping timeout: 276 seconds]
eizo has quit [Quit: Page closed]
avsm has joined #ocaml
<whitequark>
Drup: what do you need to use XMETAExtraLines?
<Drup>
but yeah, executable probably can't contain meta stuff
ddosia has joined #ocaml
wwilly has joined #ocaml
<wwilly>
salut
<adrien_oww>
morning
arjunguh_ has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
maattdd has joined #ocaml
studybot has joined #ocaml
tnguyen has joined #ocaml
gal_bolle has quit [Quit: Konversation terminated!]
studybot has quit [Remote host closed the connection]
arjunguha has joined #ocaml
maattdd has quit [Ping timeout: 252 seconds]
arjunguha has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
Kakadu has joined #ocaml
Kakadu has quit [Ping timeout: 240 seconds]
ollehar has quit [Ping timeout: 255 seconds]
darkf has quit [Quit: Leaving]
tnguyen has quit [Quit: tnguyen]
tnguyen has joined #ocaml
* whitequark
sighs
<whitequark>
ppx findlib support sent to Gerd
shinnya has quit [Ping timeout: 255 seconds]
maattdd has joined #ocaml
demonimin has joined #ocaml
Kakadu has joined #ocaml
studybot has joined #ocaml
maattdd has quit [Ping timeout: 245 seconds]
divyanshu has quit [Quit: Computer has gone to sleep.]
ollehar has joined #ocaml
rand000 has quit [Ping timeout: 240 seconds]
rand000 has joined #ocaml
arjunguha has joined #ocaml
<jpdeplaix>
whitequark: I don't really understand why is there an
<jpdeplaix>
fail
<jpdeplaix>
the llcontext type*
<whitequark>
thread safety
<whitequark>
each llcontext must be accessed from strictly one thread
divyanshu has joined #ocaml
<jpdeplaix>
mmh, fair enough
<jpdeplaix>
thanks
Thooms has quit [Ping timeout: 255 seconds]
boogie has joined #ocaml
Nuki has joined #ocaml
ollehar has quit [Ping timeout: 255 seconds]
<jpdeplaix>
whitequark: what is the linker's behavior if two functions or globals have the same name in both modules ?
<jpdeplaix>
(sorry for all those questions :D)
<whitequark>
hrm
<whitequark>
it renames one of them
<whitequark>
(unless you explicitly specify one global as external, that is)
boogie has quit [Remote host closed the connection]
rgrinberg has joined #ocaml
boogie has joined #ocaml
boogie has quit [Remote host closed the connection]
Thooms has joined #ocaml
<jpeeters>
Hi everyone
<jpeeters>
I am trying to cross-compile on ARM the ocaml compiler for another system than Linux/Unix
<jpeeters>
nor Windows
<jpeeters>
is there a quite generic procedure on the web for cross-compiling ocaml?
maattdd has joined #ocaml
maattdd has quit [Ping timeout: 240 seconds]
tane has joined #ocaml
<adrien_oww>
there are various set of patches which aren't fully integrated yet
<adrien_oww>
what's your target?
<adrien_oww>
and
<jpeeters>
arm
<adrien_oww>
hmm
<jpeeters>
system is a custom os
<adrien_oww>
you want to build a cross-compiler or cross-compile the compiler?
<jpeeters>
with support for libc and posix
<adrien_oww>
posix? threads? native port of ocaml available?
<jpeeters>
I want to build a cross-compiler that let me compile binaries on my host computer and run them on the target
<jpeeters>
posix and threads available but no native port I think
<jpeeters>
(what do mean my native port exactly?)
<adrien_oww>
ocamlopt available
<jpeeters>
no native port of ocamlopt on the target
<adrien_oww>
Unix module usable? (and useful?)
boogie has joined #ocaml
michael_lee has joined #ocaml
<kerneis>
gasche: can you think of any reason why PPrint.ToChannel stdout would work properly, but PPrint.ToFormatter Format.std_formatter would produce a completely mangled output?
michael_lee has quit [Remote host closed the connection]
arj has quit [Quit: Leaving.]
boogie has quit [Remote host closed the connection]
maattdd has joined #ocaml
ygrek_ has quit [Ping timeout: 252 seconds]
arjunguha has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
jao has joined #ocaml
jao has quit [Changing host]
jao has joined #ocaml
Fullma has quit [Quit: Fullma]
<jpeeters>
adrien: no unix
<jpeeters>
the target is a micro-controller (Cortex-M4) and there is no notion of user/kernel thread
manizzle has joined #ocaml
ontologiae has quit [Ping timeout: 240 seconds]
arjunguha has joined #ocaml
michael_lee has joined #ocaml
eikke__ has quit [Ping timeout: 252 seconds]
manizzle has quit [Ping timeout: 240 seconds]
<gasche>
kerneis: are you using trunk or 4.01?
<gasche>
if 4.01, the main source of "mangled output" with Format are buffering problems
<gasche>
(when two pretty-printers compete on a given formatter)
<adrien_oww>
jpeeters: ok so you need to cross-compile the bytecode interpreter (which is C) and then you can build the bytecode with ocamlc; bytecode that doesn't use C primitives is portable
<gasche>
I don't see why PPrint alone would have those, though, expect bugs in the new PPrint implementation (François reimplemented it recently)
<adrien_oww>
jpeeters: you might also want to take a look at "ocapic"
<gasche>
if you're on trunk, the reason would be "the new Format implementation is possibly broken"
zpe has quit [Remote host closed the connection]
<adrien_oww>
jpeeters: I don't know if there's something that patches to cross-compile the bytecode interpreter but it's might only be that you need to set the C compiler when calling configure
zpe has joined #ocaml
tane has quit [Quit: Verlassend]
zpe has quit [Ping timeout: 252 seconds]
<kerneis>
gasche: 4.01, thanks
<kerneis>
and I use the new PPrint indeed
<kerneis>
I could try and switch to the previous one to see if it comes from there
<kerneis>
I'll send a bug report tomorrow if I can reproduce
<kerneis>
(the problem, it seems, is that at first, all strings are output, then all whitespace and symbols — very weird — and after some amount of input, the output finally becomes sensible)
<kerneis>
enough for today, see you tomorrow
racycle has joined #ocaml
jwatzman|work has joined #ocaml
ohama has quit [Remote host closed the connection]
tobiasBora has quit [Quit: Konversation terminated!]
eikke__ has quit [Ping timeout: 255 seconds]
Axman6 has joined #ocaml
ontologiae has joined #ocaml
Bynbo7 has quit [Ping timeout: 252 seconds]
ontologiae has quit [Ping timeout: 252 seconds]
<rand000>
Hello, does anyone know a way of delaying evaluation of a (module)-functor application? I'm trying to avoid using a reference to the internal state of the resulting module.. :/
avsm has joined #ocaml
<mrvn>
functorize it
<mrvn>
or pass first class modules
<rand000>
I see what you mean by functorizing - what do you mean by passsing first class module?
<rand000>
oh.. I've found a guide; thx (:
<mrvn>
You pass a module as argument to the function (or return it). That is like a functor but done manually at runtime.
<mrvn>
if the module you want to use depends on some input at runtime then you want first class modules.
<rand000>
Wow didn't know first class modules was possible :P nice
<mrvn>
hasn't been possible for too long.
<rand000>
ah
michael_lee has quit [Quit: Ex-Chat]
Arsenik has joined #ocaml
claudiuc has quit [Remote host closed the connection]
Kakadu has joined #ocaml
Submarine has joined #ocaml
Submarine has joined #ocaml
tane has quit [Quit: Verlassend]
manizzle has joined #ocaml
Eyyub has joined #ocaml
<jpeeters>
adrien_oww: thank you for your answer
<adrien>
np
<adrien>
and I hope that's pretty much all you'll have to do
<jpeeters>
adrien_oww: so I just need configure and make ocamlc right?
<adrien>
"make world"
<jpeeters>
and what about native code. It is what I am expecting for performance and limited overhead
<adrien>
I can check a couple things, I need to finish an email first
<jpeeters>
adrien: np
avsm has quit [Quit: Leaving.]
<jpeeters>
adrien: about ocapic, this is a C code generator right ?
<adrien>
native code, there's work on it; I think we can be confident for something before the end of the year (in svn)
Hannibal_Smith has quit [Read error: Connection reset by peer]
<adrien>
but first you need a port of ocaml native code to that arch
<adrien>
btw, which kernel is it?
avsm has joined #ocaml
<adrien>
as for ocapic, it's a bytecode VM that targets PIC18 (and above); it's really a bytecode VM and not a translator to C
<adrien>
some of the changes done to fit on something as small as PIC might not be good for larger applications (but maybe you're going for ARMs with no external memory)
<adrien>
in any case, porting ocapic is probably more work (it's baremetal and requires some assembly)
<jpeeters>
adrien: the kernel is a custom one that come from previous research work
<jpeeters>
writing assembly is not really a problem
<jpeeters>
the architecture is ARMv7-M
<jpeeters>
so I think that the port of ARM to the cortex-M should mostly work
<jpeeters>
adrien: about using the bytecode interpreter, I want that ocamlc runs on the host and the final binary runs on the target
<jpeeters>
how can I do that?
tlockney is now known as tlockney_away
ollehar has quit [Ping timeout: 255 seconds]
srcerer has quit [Quit: ChatZilla 0.9.90.1 [Firefox 28.0/20140314220517]]
BitPuffin has joined #ocaml
manizzle has quit [Remote host closed the connection]
<companion_cube>
the compiler should provide smart constructors to avoid this, I think
<whitequark>
the compiler should typecheck its shit more thoroughly.
<whitequark>
I mean, stuff like this makes me appreciate the value of a certified compiler.
<whitequark>
how did it happen that neither -dsource, nor typechecker, nor bytecode emitter have even a single assertion for that case?!
<companion_cube>
yeah, it should be impossible by construction
<companion_cube>
did you create the AST directly with constructors?
<whitequark>
well, duh
maattdd has quit [Ping timeout: 252 seconds]
<companion_cube>
I really favor smart constructors for this exact reason...
<companion_cube>
enforcing invariants
Nahra has quit [Remote host closed the connection]
Nahra has joined #ocaml
<companion_cube>
whitequark: still, that's a bug in an unreleased version, using a feature that is not the core language, but a preprocessor
<companion_cube>
it's not as if you wrote a regular function and it crashed
<whitequark>
companion_cube: not in core language?
<whitequark>
ppx is very much in the core language now
<companion_cube>
well ppx isn't OCaml
<companion_cube>
it's a feature of the compiler, not the language
<companion_cube>
and it's in 4.02 which is not released yet
<whitequark>
splitting hairs. as a user, I know that I only wrote code in supposedly memory-safe language and it crashed
<whitequark>
and it probably would've slept until 4.02 is released, unless I found it
<companion_cube>
in an unreleased version
<companion_cube>
maybe... maybe not :)
<whitequark>
and there are probably dozens of others
<companion_cube>
maybe the AST shouldn't be directly exposed like that...
<whitequark>
which I don't even know how to reliably find
<companion_cube>
whitequark: maintainers will see this tomorrow (gasche for instance) and fix it, and probably think about validating/sanitizing user (ppx) input
<whitequark>
(that's not the first time I report bugs related to broken invariants in AST)
<Drup>
whitequark: implicits invariants in the AST is a well know flaw
<companion_cube>
defensive programming is a thing...
<Drup>
chambar talked to me about that like one year ago, telling me it was a nightmare to fiddle with the internal because implicit invariants were breaking quite often when you were doing clever stuff
<bernardofpc>
Drup> is there a video of chambard's talk from OUPS ? -> links ?
arjunguha has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
<companion_cube>
whitequark: your next objective is to write a verified compiler for OCaml? :D
<Drup>
companion_cube: well, he did start investigating Coq.
<whitequark>
companion_cube: probably not
<whitequark>
my next objective is to build anything verified at all that is more complex than adding two Peano numbers
<companion_cube>
it's oriented toward using dependent types for programming, and verifying programs
<companion_cube>
the very first example of the book is writing a micro-compiler
<companion_cube>
(for arith expressions)
<Drup>
well
<Drup>
if it's for arith expressions
<Drup>
it's not much more than adding two peano numbers :D
<companion_cube>
tsk tsk
<companion_cube>
it adds tests in the second example
<whitequark>
a monumental achievement indeed
<companion_cube>
or a while loop, I don't recall
<companion_cube>
anyway, it's still more advanced than just evaluating the sum ;)
<whitequark>
(the fact that it likely *is* just shows how esoteric the entire field is)
darkf has joined #ocaml
S11001001 has joined #ocaml
S11001001 has quit [Changing host]
S11001001 has joined #ocaml
<whitequark>
grm
<whitequark>
I removed 0-ary applications
<whitequark>
it still segfaults
<whitequark>
...
jao has joined #ocaml
jao has quit [Changing host]
jao has joined #ocaml
<Drup>
whitequark: did you try agda/idris ?
<whitequark>
oh nevermind, outdated file
<whitequark>
Drup: nope
<Drup>
ok
<Drup>
you may be interested
<Drup>
it's a different approach than coq
<whitequark>
last time I heard about agda, I was overrun by some incredibly smug zealots
Nuki has quit [Remote host closed the connection]
<Drup>
more directed towards programming than proving.
SethTisue has quit [Quit: SethTisue]
<whitequark>
hrm. frankly, the Coq workflow of prove-then-extract somehow seems more appealing to me, and I'm interested in automated theorem proving not directly related to programming as well
<whitequark>
but I'll think about it
<Drup>
it's still interesting anyway :p
<whitequark>
there's only so much hours in a day...
<companion_cube>
idris looks still very young tho
<companion_cube>
Drup: funny because now there's at least one real program written in coq (that I'm aware of)
<Drup>
companion_cube: well, probably because it *is* very young
<whitequark>
companion_cube: which one?
<companion_cube>
are there real programs written in agda?
<companion_cube>
whitequark: compCert
<whitequark>
btw, ocaml-msgpack is a real program that is written in coq
<whitequark>
it's horrible though, but it looks like it would work
<Drup>
companion_cube: in Agda ? hell no
<whitequark>
and it's just some random example I accidentally ran into
<companion_cube>
wow, impressive
<Drup>
the extraction is inefficient as hell.
<Drup>
well, actually, there are
<Drup>
but not very interesting by them self
<companion_cube>
Drup: the part of cpdt I read impressed me, especially subset types
<companion_cube>
it looked almost usable for programming :D
<Drup>
beware of this kind of statement
<Drup>
you might actually get it into a programming language
<companion_cube>
I meant, coq looked almost usable for programming, using subset types and the likes
avsm has quit [Quit: Leaving.]
<companion_cube>
but now I need to focus on complicated, buggy ocaml I write for my thesis
<Drup>
companion_cube: did you actually tried to write something of a reasonable size in Coq ?
<Drup>
(by yourself, not following a tutorial)
* whitequark
shudders
tobiasBora has quit [Quit: Konversation terminated!]
<companion_cube>
not yet
<companion_cube>
I need to find something to do with it
<Drup>
yeah, not surprised :p
<companion_cube>
I feel ignorant compared to people who know coq well :)
<Drup>
the grass is greener ... :p
<companion_cube>
(or type theory in general)
<whitequark>
companion_cube: write a web browser
<companion_cube>
awwww
<companion_cube>
no, certainly not!
<whitequark>
why would you pass such an opportunity at falling into complete despair?!
<Drup>
companion_cube: there is actually a certified html renderer.
<companion_cube>
I should write a smallish, certified automated theorem prover in coq
<Drup>
whitequark*
<whitequark>
Drup: I think I've heard
<Drup>
whitequark: and some people are working on a javascript certification
<companion_cube>
oh dear
<whitequark>
Drup: I think they've been successful
<companion_cube>
some people really want to get mad
<Drup>
(which would naturally yield to a certified intepretor)