One-liner segfault

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#3831
From: @maximedenes
Reported version: 8.5
CC: @aspiwack, @gares, @gasche, @silene, @herbelin, @mattam82, @letouzey

[coqbot]

Comment author: @maximedenes

Welcome to Coq trunk (87f9997)

Coq < Show Proof.
[1] 6037 segmentation fault (core dumped) coqtop

[coqbot]

Comment author: @maximedenes

After more investigation (with the help of Gabriel), the bug occurs only under OCaml 4.02.1 (not 4.01), and is due to PMP's code for exception handling in lib/exninfo.ml. Turning these functions into identities makes the problem disappear.

My guess is that any uncaught exception will trigger a segfault (nothing specific to Show Proof, which is just raising NoCurrentProof in this case). Gabriel says that the representation of exceptions has changed in 4.02.

[coqbot]

Comment author: @gares

Maxime, while you have Gabriel at hand, please ask him how to obtain the same
feature PMP did hack, possibly in a more clean/robust way.

Having the possibility to load an exception with extra info is extremely
useful. E.g. you can localize the exception to a piece of text by adding a Loc.t, you can make it refer to the system state that failed by adding a Stateid.t, etc... Without such feature you are forced to pollute the code
with stuff like

exception WithLoc of Loc.t * exn
exception WithState of Stateid.t * exn

and then your exception handling code becomes a huge mess

with Foo | WithLoc (,Foo) | WithState(,Foo) |
WithLoc (, WithState (, Foo)) |
WithState (, WithLoc (, Foo)) -> ...

(that is what the code looks like in Matita...).

Of course having such feature be integrated upstream would be awesome.

If it is impossible or rejected, we could fix the code having just
one exception wrapper containing a ref to a list of Dyn.t

exception WithInfo of Dyn.t list ref * exn

with Foo | WithInfo(_,Foo) -> ...

Better than the code above but still very ugly.

[coqbot]

Comment author: @ppedrot

I remember that Jacques-Henri coded such a thing, but it was using a global imperative table to register data, which I find rather ugly (and not working properly in the debugger any way, because it is not marshalled at the same time).

What is the current implementation of exceptions in OCaml 4.02?

[coqbot]

Comment author: @gasche

What is the current implementation of exceptions in OCaml 4.02?

You sound like a dilettante bank robber that meditates in jail, instead of his reinsertion, about how to rob it better next time.

Jacques-Henri indeed worked on a similar topic last year, as explained in this blog post about his prototype library:
http://gallium.inria.fr/blog/a-library-to-record-ocaml-backtraces/

(Note: the worrying performance numbers reported in the post are about what happens if you use syntactic preprocessing to store traces on all try..with constructs. A version that manually implements logging only in some well-chosen case, as already done in the Coq codebase, would control the cost in a much more fine-grained way.)

The interface he relied on are now part of OCaml proper (the raw_backtrace part that allows it to be efficient is present since 4.01; 4.02 adds a way to get the call stack (not necessarily at exception-raising points) in the same raw format, and inspect it from user code), thanks to work by him and Alain Frisch that also needed this feature.

I can't comment on the suitability of the global table as I don't know much about ocamldebug. I'd note that it can be thought of as a persistent mapping, however: keys are (linearily) looked up by physical comparison with the raised exception, so it should be robust to insertion side-effects (not) being backtracked.

(On the other hand, his work assumes that two exceptions raised at different times are physically distinct, which I'm not sure is still true with the new representation of exceptions.)

[coqbot]

Comment author: @ppedrot

You sound like a dilettante bank robber that meditates in jail, instead of
his reinsertion, about how to rob it better next time.

I better like to be thought of as a Bernard Madoff!

I can't comment on the suitability of the global table as I don't know much
about ocamldebug. I'd note that it can be thought of as a persistent
mapping, however: keys are (linearily) looked up by physical comparison with
the raised exception, so it should be robust to insertion side-effects (not)
being backtracked.

This is a problem of locality, not of backtrack. Everything running from the side of the program being debugged is not seen in the debugger, except for the values immediately accessible, that are actually remotely marshalled to the debugger. So any non-local info is lost. This is what happen with the current implementation of ephemera in Coq, which uses the same global table technique instead of a proper implementation in the GC of OCaml.

So I would be better off with global hacks like this.

(On the other hand, his work assumes that two exceptions raised at different
times are physically distinct, which I'm not sure is still true with the new
representation of exceptions.)

I had a quick look at the trunk code of OCaml. I believe we can port the current hack to the 4.02 branch, and dispatch the behaviour according to the version of OCaml at initialization time.

[coqbot]

Comment author: @gares

The argument about ocamldebug is pretty void in my opinion. ocamldebug never works for me and nobody uses it as far as I know (for Coq).
It is dead slow on non trivial Coq files. Pierre B. tried to use it at some
point to debug unification problems in the Math Comp library and he was literally
running to the breakpoint over night.
And even when the test case is short, I always see the others using Drop + #trace.

I would recommend using the implementation that makes the least set of
assumption over the runtime. What you seem to propose may break in
4.03, for the very same reason it broke in 4.02, and then you will be back casting a voodoo spell. Please, code something as future proof as possible
(even if this makes the exn-info not accessible to ocamldebug).

Best,

[coqbot]

Comment author: @ppedrot

The issue is deeper than I thought. As Gabriel made the remark, pointer uniqueness for exceptions does not hold anymore.

Essentially, I cannot fix my code for exceptions without arguments, because since 4.02, any two such exceptions with the same constructor (e.g. Exit) share the same pointer, that is, Exit == Exit, which was not the case before 4.02. The semantics of the language rely on this fact, so that we cannot modify such argument-free exceptions in place by adding a new field as I did before.

Even worse, this also prevents Jacques-Henri's global table solution, for the very same reason of sharing the same code. I do not know how to fix this properly. The simplest solution is to add a dummy unit argument to arguments-free exceptions that should wear information, and to tweak the enriching mechanism to ignore arguments-free exceptions otherwise.

As we say, « Bref, c'est la merde. »

@ Gabriel: do you know why the OCaml implementation was changed like this in the first place? It seems to me really strange that we handle separately no-arguments exceptions vs. arguments-wearing exceptions (and, since 4.02, open variants). Is it for efficiency reason? Would it be ever conceivable that OCaml could backtrack on this precise point? I am not argueing against the other changes of representation of exceptions, just the fact that at least distinct exceptions should create distinct pointers.

[coqbot]

Comment author: @gares

Can we redefine raise and have a 1 slot info bucket somewhere?

Something like "raise ~info e" setting the info and "raise e" just
erase the old info if present and "re-raise e" to raise without erasing?

In other words having the exception api hold the value, and not the exception itself.

[coqbot]

Comment author: @ppedrot

We can try to do that indeed. This is not thread-safe, but it should not be a problem.

For the record,

http://caml.inria.fr/mantis/view.php?id=6683

I think Xaxier never looked at the code of Coq, otherwise he would be much more horrified...

[coqbot]

Comment author: @gares

Well, being thread safe is actually relevant since I do use threads for the STM.
They do use some exceptions, but I could rewrite things to use an option type
if really needed.

[coqbot]

Comment author: @ppedrot

Well, if you can do that, I would be pleased. The few other uses of enriched exceptions can be rewritten in an slightly unsound way with global state (that is, potentially mistaking argument-free exceptions), but this should be sufficient for debugging purposes. I am mainly concerned by the uses of the STM which seem nontrivial to me...

[coqbot]

Comment author: @gares

Well, Xavier is right: if you depend on undocumented features then you are alone.

We are in trouble. The approaches discussed here that try to keep the code
as it is are fragile:

• the global table one is error prone because if you declare an exception
  with no arguments than things break silently, and we can't detect it.
• redefining raise cannot be done easily because we are not systematically
  using a preprocessor for every file, it is not thread safe and calling raise
  instead of re-raise would introduce a silent error.

So I see no other option than going back to wrapping an exception into another
one to enrich it, place this wrapper in exninfo together with some APIs and port
the code to that. I can surely do that for the STM, but someone has to do it
for Loc (and all the other uses of exninfo I'm not aware of)...

The lesson we should all learn is to complain early when we see this kind of
trickery committed in the repository, and promptly revert the commits.

The lesson PMP should learn is to stop doing that once an forall.

At the light of this episode I find compulsory to know the list of hacks that rely
on undocumented OCaml features. I recall one in Intmap (that depends on the actual
implementation of an opaque data type in the stdlib), but there may the others...

Best,

For the records, the STM adds to the exception 2 Stateid.t values (the state we
were trying to reach and the last state we managed to reach). The enrichment
function is also stocked into the future computation so that when one manipulates
the future (like stocking it in the env) and encounters an error, he can enrich
the exception he wants to raise in the same way the Future.computation would
have enriched an exception happening during the computation.

[coqbot]

Comment author: @ppedrot

In OCaml 4.02 we can discriminate arguments-free exceptions at runtime, so that we could do a hybrid approach.

1. Keep the actual system, or use a cleaned-up version with a global table relying on pointer equality for exceptions with arguments.

2. Ignore additional info worn by argument-free exceptions, potentially raising an assertion failure if the info was required.

For debugging info, ignoring exceptions should be sufficient. If there is code deeply relying on the content of the information, well, it has to be rewritten (STM ?).

Wrt. the hack of Intmap, there is an easy solution, which is to import in the code our own version of the maps...

[coqbot]

Comment author: @gares

STM use exninfo for error reporting, exactly as the parser or the pretyper attach to the exception a Loc.t to identify the subterm or substring that does not type or does not parse. STM adds to that the system state id. In other words, if you put a sentence per line, the state id is pretty much the line number while the Loc.t is the offsets in that line.

I can use a wrapper exception in STM, and we can go back to a wrapper exception for Loc.t as well (after all, it was like that before exninfo). I can try to do that next week (for the STM) and see how it goes.

For handling the backtrace I'm unsure not being able to deal with arguments free exceptions is good enough. Tracing Not_found seems important to me.

I don't know know if there are other users of exninfo.

I agree that embedding the code of map.ml is a solution, and should probably be done, or we risk Coq compiling but not working with a future OCaml version that changes the implementation of Map.

[coqbot]

Comment author: @gares

I did experiment a bit, both the Wrap exception idea and the global table one.

https://github.com/gares/coq/tree/try/wrapexn
https://github.com/gares/coq/tree/try/exntab

None of them just works but the second one is promising, since it almost works:
backtraces are there and the STM correctly reports the error on the right line,
but for some reasons I did not investigate the location of type errors is lost.
Of course it suffers the == problem PMP explained and also there is some risk
of having garbage info around if one starts/kills many threads (this last
point could be fixed with a smarter implementation, but not the == one that IMO can only be mitigated by flushing the table each time one finishes interpreting a sentence).

The Wrap exception could probably work, but detecting where the code should
"try ... with (Foo.. | Wrap(_,Foo..)" instead of just matching Foo is not
trivial, and even if we get the current code right, I'm afraid it will be
hard to keep it correct in the future since no language feature seem to help
detecting that kind of mistakes. E.g. there are already functions identifying
class of exceptions, like Errors.noncritical or Pretyping_errors.precatchable_exception, but they are no used everywhere...

I did not even try to measure the impact on performances.

[coqbot]

Comment author: @ppedrot

I think the second patch is the way to go. With a little bit of modification, it should go smoothly and (almost) soundly. In particular, I would like to export the type of exception information in Exninfo, together with a user-defined raise of type

val raise : ?exninfo -> exn -> 'a

and tweaking the type of Errors.push to be

val push : exn -> exn * exninfo

so that we can easily see when enriching exceptions. Likewise, the `Exn constructor in Future should contain a pair (exn * exninfo) instead of just an exception. Do you want me to write it out an propose a pull request?

[coqbot]

Comment author: @gares

Sure, go ahead an post your branch url

[coqbot]

Comment author: @ppedrot

Here is an alternative and (I hope) sounder version.

https://github.com/ppedrot/coq/tree/pure-exninfo

Instead of adding information to arbitrary exceptions, we only do so at raise time. There is an instrumented (thread-safe) raise that sets a thread-specific reference to be the latest data set. When recovered in a try-with clause, the information is pushed back semi-automagically thanks to the Errors.push function. This is done through a dedicated enriched exception type, which is no more than an exception together with a dedicated enrichable type.

A few functions had their signature changed, to cope with this. Future exception fixing functions now take enriched exceptions, and likewise, the tactic monad does everything through enriched exceptions.

There may still be very rare cases of mismatching exceptions, but this is now more robust than just checking for pointer equality. The scenario leading to such a confusion is highly unlikely, see the Exninfo module for details.

Any comments welcome.

[coqbot]

Comment author: @gasche

That seems reasonable. I had a few comments while having a very quick look at the code:

• you comment that physical equality "slightly unsound", but if I'm not mistaken it is not "unsound" in the sense you are usually guilty of, but only incorrect from a specification point of view (it's still type-safe, memory-safe, etc.). I'd just use "incorrect" in that case.

• the names "raise_with" and "print_with" are rather bad: with what? Why is there a single parameter if I raise with something (presumably something else). What about "raise_with_info", "raise_info", "informed_raise", or just "iraise" (to match "iexn"), instead?

• you use "Exninfo.raise ~info e" instead of "iraise (info, e)" in many places, including places where the tuple is already named and using iraise would thus give shorter code. Why define an auxiliary function if you don't use it consistently?

• if you decide to consistently use "iraise", why not remove the optional ?info parameter of "raise", and only use it when there is no information available?

[coqbot]

Comment author: @ppedrot

• you comment that physical equality "slightly unsound", but if I'm not
  mistaken it is not "unsound" in the sense you are usually guilty of, but
  only incorrect from a specification point of view (it's still type-safe,
  memory-safe, etc.). I'd just use "incorrect" in that case.

Well, not respecting a specification is in particular unsound, but this is nitpicking, isn't it?

• the names "raise_with" and "print_with" are rather bad: with what? Why is
  there a single parameter if I raise with something (presumably something
  else). What about "raise_with_info", "raise_info", "informed_raise", or just
  "iraise" (to match "iexn"), instead?

I took the first name that popped in my head. You can change it as you wish.

• you use "Exninfo.raise ~info e" instead of "iraise (info, e)" in many
  places, including places where the tuple is already named and using iraise
  would thus give shorter code. Why define an auxiliary function if you don't
  use it consistently?

Erm, the iraise function is only defined in Util, which is at the end of the clib file. All files using Exninfo.raise are in lib/, hence before the iraise. But it is indeed possible to defined the iraise in the Exninfo file itself and reexporting it in Util.

• if you decide to consistently use "iraise", why not remove the optional
  ?info parameter of "raise", and only use it when there is no information
  available?

Do as you like. This patch was a proof of concept, not a push-ready one.

[coqbot]

Comment author: @ppedrot

BTW, after a glance at the STM code, I am unsure that we need the full power of built-in threads (and thus, all of the thread-safety boredom that comes with it). It seems that what we only need is essentially cooperative non-blocking IO.

Enrico, do you think it is feasible to write a tiny (hopefully monadic) lightweight-thread library allowing to implement the STM without polluting all the code with the threaded behaviour?

[coqbot]

Comment author: @aspiwack

Speaking of which. Can I ask, very ignorantly, why we need threads/mutexes to begin with? I thought the stm only used forks and stuff. Where do mutexes come into action?

[coqbot]

Comment author: @gares

OCaml threads, being non-parallel, are good only for non blocking io, exactly as coroutines, but OCaml provides the former, not the latter (that I like too).

I've used threads because it is simpler to have a thread managing a worker
than having a gigantic loop around a Unix.select, and a first order representation of the stack (with threads/coroutines you also get a stack, when you yield such stack is saved somewhere).

Worker managers are mostly pure. They interact with the rest of the world in the following ways: they pick tasks from a TQueue, they snapshot (read a !ref) the stm document, they marshall a piece of the document to the worker, they read back the proof terms, they assign a future value (a ref only the worker manager has write have access to), access RemoteCounter (a worker needs some fresh universe levels, he asks the master for them) and finally writes (forward) stuff on the feedback bus. Locks are needed in the TQueue (producer consumer), the remote counter and the feedback bus (read/write a shared var).

Well, I'm sorry I'm repeating myself once again but Coq is written in OCaml
and that language does not understand monads, type classes nor coroutines.
Writing code in a style that is not supported by the language is a PITA.
No, I'm not rewriting everything in mixture of paradigms not supported by
OCaml to spare you a boring mutex (that by the way you already wrote).

I'm also curious to ear which problem a monadic interface would solve here.

[coqbot]

Comment author: @ppedrot

Well, I'm sorry I'm repeating myself once again but Coq is written in OCaml
and that language does not understand monads, type classes nor coroutines.
Writing code in a style that is not supported by the language is a PITA.
No, I'm not rewriting everything in mixture of paradigms not supported by
OCaml to spare you a boring mutex (that by the way you already wrote).

You seem to have suffered a childhood trauma involving monads, don't you?

Monads by themselves do not require anything special in the target language to be actually used. Haskell does add syntactic sugar and typeclasses, but we need neither of both to write monadic code properly.

In practice, you did already introduce monads in Coq under the form of futures, which (almost) follow a monadic interface. The almost is there because you prefer to use the dangerous map + run (chain + force, in your parlance) combination instead of the usual bind, but that's about all.

If this is the word "monad" that bothers you, just change it into "computation" or whatever pleases you. Actually most of involved OCaml code out there uses some form of monad, but it does not usually advertise it with a huge blinking signal. I clearly remember that for instance, there are monadic structures in the ocamlnet library, without having the word "monad" spelled out once.

I'm also curious to ear which problem a monadic interface would solve here.

This is not about monads: this is about being able to know statically when we're in threaded code, and when we are not. I find it rather stupid to depend on the Thread library, and to change the whole model of execution of Coq, just for three calls or so to non-blocking IO, drowned in a sea of sequential code.

Here, we could just embed those three calls into a small non-blocking IO library, using the standard CPS-style transformation, with a proper event-handling loop running that stuff at the very end. That would save us a lot of hassle about thread safety. And no, this is not about mutexes: this is about changing globally the semantics of the programming language.

This is also the proper moment to finish with a trollish quotation about S(T)Ms.

"Computer is a state machine. Threads are for people who can't program state machines." (Alan Cox)

[coqbot]

Comment author: @gares

The fact the new monadic API has almost eaten up all the performance
optimizations you did is what I mean by "the language does not support this
style of programming". Correct me if I'm wrong please, but this is the
impression I got looking at the oscillations in the time charts.

I don't like threads, in general they just mess up the code.
I think the use I made of threads is quite legitimate and not very
complex either.
And I'm not so sure I changed the semantics of the programming language,
threads are part of the OCaml language. For sure it is not worse than
relaying on undocumented features.

I'm sorry fixing the exninfo mess turns out to be harder because I'm using threads. All you say about rewriting everything in a different style is surely
doable, but I'm afraid you underestimate how much time it would take.

If you really want the citation (you know who said that, I guess):
Talk is cheap, show me the code.

[coqbot]

Comment author: @ppedrot

The fact the new monadic API has almost eaten up all the performance
optimizations you did is what I mean by "the language does not support this
style of programming". Correct me if I'm wrong please, but this is the
impression I got looking at the oscillations in the time charts.

I believe you are talking about the Ltac monadic API? Then that is untrue, or at least not because of the monad itself. From what I have seen in real code, the additional hotspots of the current trunk are (by decreasing order of magnitude):

1. Handling of universes in evar maps
2. Changes in unification
3. Nf-evarization of terms in tactic

Only the third point is somehow related to the change of interface, but this has nothing to do with the fact we are monadic. It is here for compatibility purpose, and is going to disappear when we switch all tactics to the monad.

I actually believe the converse, that is, the monad (in its current form) is slightly quicker than the old hand-written monadic-ish code. This is due to its careful crafting, with the CPS-based encoding which is essentially free.

(BTW, we should do something about 1. in Ssreflect, it is a pity to have 20%~25% of the time due to the ugly merge of universes when one could do it for free in state passing style.)

I don't like threads, in general they just mess up the code.

+1

I think the use I made of threads is quite legitimate and not very
complex either.

It is, indeed. I am just advocating the fact that we may think of restricting it out of the STM.

And I'm not so sure I changed the semantics of the programming language,
threads are part of the OCaml language. For sure it is not worse than
relaying on undocumented features.

Threads do change the semantics of OCaml. As delimited continuations from delimcc do (fwiw, there was an interesting thread on the Caml list about delimcc used together with the imperative trick of tail-rec list map, wreaking havoc). Being a library does not mean it does not mess with the operational semantics of the language.

I'm sorry fixing the exninfo mess turns out to be harder because I'm using
threads. All you say about rewriting everything in a different style is
surely
doable, but I'm afraid you underestimate how much time it would take.

This is not directly related to the Exninfo. This was just a side remark, considering I do not like threads and the use we make of them seems really reducible to a few simple primitives.

If you really want the citation (you know who said that, I guess):
Talk is cheap, show me the code.

When I'm done with my thesis!

[coqbot]

Comment author: @aspiwack

Enrico: one possible way of representing non-blocking IO is futures. This is in the most abstract and non-definite sense of the word. But I still wonder whether your futures would be able to abstract over the asynchronous system calls you use. The secondary question is, of course, whether that would be desirable.

On the efficiency concern, Lwt has proved that cooperative concurrency is, in general, significantly more efficient than threads, despite the higher-order encoding. For reference, they have non-blocking IO too [ http://ocsigen.org/lwt/2.4.3/api/Lwt_unix ]. I must confess I know neither how they work or how they are implemented.

[coqbot]

Comment author: @gares

@ Arnaud: A future is like lazy_t but you can create it in two ways:
with a closure (when you force it, you compute it) or via a delegate (gives
you the future + an assignment function). When you create a future of
the second kind you enqueue the assignment function + a job description
into a task queue. Worker (their manager thread) is popping tasks from
the queue, send them to the real workers via a socket and assigning back
the result when it comes back.

So the non-blockingness is given by the fact that the blocking call
(to a socket receive) is performed by a thread. The alternative is
to not do the read, add the socket descriptor + a continuation to a pool,
do a select, depending on the fd that is readable pass the ball to the corresponding continuation and let it do the read (that won't block).
All in all is about having an implicit "save/restore" of the stack, either
the OS does it, or the CPS encoding.

One last remark, it is not about efficiency here. What costs is marshalling
the state, sending it via a socket, etc. The cost of context switching
or locking is not relevant IMO. Anyway if you have a reference paper with
the benchmarks I'd be happy to read it.

[coqbot]

Comment author: @aspiwack

So I was suggesting to implement futures using futures… Well, that was kind of silly. I don't actually know if a thread-free version of the worker manager would be better than the current one. I don't really have time to understand Lwt's implementation of non-blocking IO and whether, in particular, it would free the rest of the code from locks.

I don't have any experimental result on cooperative interfaces vs threads. It's just empirically faster to use Lwt rather than thread-intensive computation (that said, our case does not qualify as thread-intensive, so who knows). I don't think that's very important, I just mentioned it because you seem to be worried about efficiency of higher-order interfaces yourself.

[coqbot]

Comment author: @gares

No, not in my code. I was pointing the finger at monads because I have the impression one piles up closures, allocations. Actually my understanding
of your bootstrap/ code was that indeed ocamlc did not optimize code that
a compiler monad-aware would have optimized. And such optimization
was reducing dummy redexes under lambdas...

I have 1 future per proof, something like 5 chained functions each, and say
1000 proofs for file. I don't think the allocation of a 5K closures is visible.

But my guess was that doing so at each "tactic/tactical call" would be
noticeable.

[coqbot]

Comment author: @gasche

• you comment that physical equality "slightly unsound", but if I'm not
  mistaken it is not "unsound" in the sense you are usually guilty of, but
  only incorrect from a specification point of view (it's still type-safe,
  memory-safe, etc.). I'd just use "incorrect" in that case.

Well, not respecting a specification is in particular unsound, but this is
nitpicking, isn't it?

Indeed; what comes out of a review when one doesn't understand the high-level stuff is usually the details -- nitpicking. But the details do matter.

• the names "raise_with" and "print_with" are rather bad: with what? Why is
  there a single parameter if I raise with something (presumably something
  else). What about "raise_with_info", "raise_info", "informed_raise", or just
  "iraise" (to match "iexn"), instead?

I took the first name that popped in my head. You can change it as you wish.

I'm not sure what you mean by "You can change it", I'm not going to do the work of evolving this pull request into something "push-ready", and I kind of assumed that you would be in charge of that. Assuming this means "change it by giving me a strong opinion that I will follow because I don't care that much", I suggest you use "iraise".

Erm, the iraise function is only defined in Util, which is at the end of the
clib file. All files using Exninfo.raise are in lib/, hence before the
iraise. But it is indeed possible to defined the iraise in the Exninfo file
itself and reexporting it in Util.

Yes, that would be better.

• if you decide to consistently use "iraise", why not remove the optional
  ?info parameter of "raise", and only use it when there is no information
  available?

Do as you like.

After more though, I think the best move is actually to make the parameter non-optional at type (info option) (labelled or not). This means that people using raise in this scope will be forced to think about whether they have information available or not, as they should.

[coqbot]

Comment author: @ppedrot

I have cleaned up this patch a bit, and make it compile properly on the test-suite. Yet, I am currently experiencing two issues.

1. Vi file compilation in the test-suite fail because the structure of the objects have changed, and the checker complains. I assume this is innocuous, but I do not know where to look exactly to fix this. Enrico, do you have any pointers?

2. I had a more serious issue, that I came upon while debugging a stupid bug I had inadvertently introduced. For some unknown reason, the debugger is now slow as hell. I conjecture this has to do with the introduction of threads everywhere, but I do not see exactly why this would wreak havoc like so. I thought the debugger only sympathetically forked to retain the previous states. How can threads mess up with this? Gabriel, do you have any idea on the source of this situation?

Apart from this, I am fairly satisfied about this patch. On the few files I have tested, I cannot see any overhead in compilation time. This is no scientific benchmarking, but the patch seems neutral.

I did not integrate Gabriel advises yet. I am rather happy of the "iraise" name, but I am not too fond of the compulsory option argument of raise. It looks ugly. Further comments anyone?

[coqbot]

Comment author: @gares

w.r.t. 1, this is expected. I expect Matthieu to fix the format description for universe related fields at some point ;-)

Is the patch at the usual place? It seems not up do date since it says that the last commit is 8 days old. Did you push?

[coqbot]

Comment author: @gasche

I am not too fond of the compulsory option argument of raise. It looks ugly.

If you make the argument optional, you must be prepared to the fact that people that write code and are unfamiliar with the API will never set it. The only way to make them think after which value they want to pass is to have the type-checker if they don't pass one. I think it's fine if people have to think twice before raising an exception -- they will have to think about where it will be caught, and this will reduce the number of bugs.

[coqbot]

Comment author: @ppedrot

Is the patch at the usual place? It seems not up do date since it says that
the last commit is 8 days old. Did you push?

Yep, I rebased the patches before pushing, thus keeping the old commit date. I know this is bad practice when the branch is public, but this patch is not merge-ready yet so I do not care that much.

[coqbot]

Comment author: @ppedrot

Strange... I can't reproduce the slow behaviour of ocamldebug... Maybe the program was in a eldritch state? So, apart from the vi file & the renaming of functions, this patch should be OK then.

[coqbot]

Comment author: @gares

I'm sympathetic to the proposal of Gabriel, but I'm afraid it is too late now.
If we put in Util (opened everywhere) a raise function that has a different type
then it will take a month to PMP to have Coq compile again :-/

[coqbot]

Comment author: @ppedrot

We can integrate this feature afterwards anyway. For now, I believe my branch is push-ready. Enrico, do you think you can port the vi checker before I push it, or do I push it quickly and we'll see afterwards?

[coqbot]

Comment author: @gares

Matthieu has to do it, the data structures one has to describe are the one of universes...

[coqbot]

Comment author: @gares

Sorry, half answer. I had no time to check your patch, but push it.
The checker is an orthogonal problem.

[coqbot]

Comment author: @gares

The compilation of ml files via coq_makefile is broken (no -thread I guess)

[coqbot]

Comment author: @silene

I cannot reproduce it, so I assume it has been fixed. If not, please reopen and provide a test case.