search

jrh13 / hol-light

The HOL Light theorem prover
Other
435 stars 79 forks source link

A fix for an OCaml >= 4.06 (?) bug in realanalysis.ml #53

Closed monadius closed 5 years ago

monadius commented 5 years ago

I think it is an OCaml bug. It can be easily reproduced with the following code in OCaml (HOL Light is not required at all) (tested with OCaml 4.06.1 and 4.07):

let rec f =
  let s t = t in
  let rec f t = s t
  and g a = a in
  f;;

Gc.minor();;

f 0;;

This code crashes OCaml with "Segmentation fault: 11" (both the toplevel and the compiled code).

jrh13 commented 5 years ago

Thanks for that fix: now merged in. A surprising change!