search

JacquesCarette / hol-light-qe

The HOL Light theorem prover (moved from Google code)
Other
7 stars 1 forks source link

Compiling OCaml code? #5

Closed laskowsp closed 7 years ago

laskowsp commented 7 years ago

I'm trying to trace through the program to find the source of some of the bugs I'm encountering, and it seems like the only way to debug the program or even get a stack trace is by compiling the program with the -g option.

How would I go about compiling HOL? It seems to use various statements the ocamlc compiler doesn't recognize, namely, it fails on the first file, system.ml because of the use of a #load directive, and I'm sure there will be other issues once this is fixed.

JacquesCarette commented 7 years ago

Hmm, it is definitely a bad habit to use #load in ocaml code! But we're unlikely to be able to fix that so easily.

My feeling would be to sprinkle some print statements here than there. You can always rename foo to my_foo and create a new

let foo a b c =
  begin
    print "entering foo";
    let res = my_foo a b c in
    begin
      print "exiting foo";
      res;
    end
  end

(you can use parens instead of begin/end if you wish). And can print more stuff along the way too.

We could also ask John Harrison how he debugs his stuff.

laskowsp commented 7 years ago

Thanks, that seems like a good enough substitute!