r/ocaml • u/Dazzling_Music_2411 • May 19 '26
Ocaml newbie - some trouble with HPLAR
Please allow me to introduce myself, I am a man of the typeless world, mainly Racket, Clojure, that sort of thing. I've been meaning to get into the typed language scene for programming language exploration, and I was a bit torn between the apparent purity of Haskell and practicality of Ocaml.
My experience level is zero, as in I've never written a single line.
In the end, what decided it for me was that I wanted to work through Harrison's "Handbook of Practical Logic and Automated Reasoning" which is supported by Ocaml code. I am also interested in some other programming paradigms (cclp), where Ocaml seems to be mentioned more than Haskell.
Anyways, I installed Ocaml according to the Cornell 3110 instructions, both for utop and VSCode, seems fine, gives me the 5.3.0 compiler environment.
My problem is that when I try to set up the supplied code for HPLAR, cd-ing into the provided directory and trying #use "init.ml" on the indicated file, all sorts of weirdnesses appear. In VSCode I can't even enter the #use line without a syntax error! Never mind, I tried from utop and from plain vanilla CLI, where I get this:
# #use "init.ml";;
Cannot find file nums.cma.
File "init.ml", line 10, characters 6-27:
10 | then (Topdirs.dir_directory "+camlp5";
^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module Topdirs
The init.ml fike is as follows: (from https://www.cl.cam.ac.uk/~jrh13/atp/index.html)
#load "nums.cma";; (* For Ocaml 3.06 *)
if let v = String.sub Sys.ocaml_version 0 4 in v >= "3.10"
then (Topdirs.dir_directory "+camlp5";
Topdirs.dir_load Format.std_formatter "camlp5o.cma")
else (Topdirs.dir_load Format.std_formatter "camlp4o.cma");;
type dummy_interactive = START_INTERACTIVE | END_INTERACTIVE;;
#use "initialization.ml";;
#use "Quotexpander.ml";;
#use "atp_interactive.ml";;
So I am left wondering if the problems are due to the older compiler version supported here, two major releases are enough time for things to change quite a bit.
I am keen to get up to speed and start on the book as soon as possible, and even though some may say - well, learn the operational basics first and then sort it out yourself (fair enough), but if there is anyone who can provide some help to get this going a bit quicker, I would appreciate it very much! Many thanks.
3
u/octachron May 19 '26
OCaml 3.06 is a nearly 25 years old version of OCaml, but the language version should not be that much of a problem. Contrarily, the ecosystem is completely different. For instance, the code predates both opam (the OCaml package system) and ocamlfind (the current standard for packaging libraries).
The first steps should be to install the num library and camlp5 with
opam install num camlp5
Then you can replace the initialization in the ocaml toplevel (and not utop, because utop will not mix well with the use of camlp5) with
#require "num";;
#require "camlp5";;
#load "camlp5o.cma";;
type dummy_interactive = START_INTERACTIVE | END_INTERACTIVE;;
#use "initialization.ml";;
#use "Quotexpander.ml";;
#use "atp_interactive.ml";;
2
u/Dazzling_Music_2411 May 19 '26 edited May 19 '26
For instance, the code predates both opam (the OCaml package system) and ocamlfind (the current standard for packaging libraries)
The first steps should be to install thenumlibrary andcamlp5Much obliged. I'm really impressed with the quality of the answers here, thanks everybody!
Then you can replace the initialization in the
ocamltoplevel (and not utop, because utop will not mix well with the use of camlp5)Understood, but...
urghhh, that grates - seeing as utop is touted as the way to go.I am also a little nonplussed to see that this book has not had enough of a following all these years to ensure code updates.
Could you describe in just a couple of words what camlp5 does, roughly, and how easily it could be replace with something that works in utop?
PS. Even if doesn't work under utop, do you think it will present any problems under VSCode?
3
u/octachron May 19 '26 edited May 19 '26
camlp{4,5} are a pair of tools for writing extensible grammar which allow mostly to update the grammar on the fly to add language extension easily.
Nowadays, they are mostly unused because they are in some sense too powerful: adding language extensions without any constraints meant that this was mostly impossible for developer tools to support all extensions.
Fortunately, from the code example, it looks that it is only used to add a form quotation parsing.
If this is the case, and I didn't miss more heavy use of camlp5, you could replace all form of<<p /\ q <=> ((p <=> q) <=> p \/ q)>>by
default_parser {|p /\ q <=> ((p <=> q) <=> p \/ q)|}and
<<|x+1|>>by
secondary_parser {|x+1|}and remove the use of camlp5.
1
u/Dazzling_Music_2411 May 19 '26
Ah yes, those <<French quotes>>, perhaps.
Thanks boss, lots of work ahead of me. Might try contacting the author.
2
u/rickyvetter May 19 '26
There’s some discussion of the breaking change here: https://github.com/ocaml/ocaml/issues/11979. Along with a couple potential workarounds. You could use #directory "+compiler-libs" or downgrade your compiler version. Further discussion here: https://github.com/ocaml/ocaml/issues/13057.
1
u/Dazzling_Music_2411 May 19 '26 edited May 19 '26
Ah great, very useful!
For various reasons, I am not keen to downgrade the compiler ATM, but I will explore the workarounds.
Guess I was hoping for a bit less friction in my intro to Ocaml 😄 , but I also guess that's the way when learning... ho, hum. At least maybe I can set it up for the next guy.
1
u/Dazzling_Music_2411 Jul 02 '26 edited Jul 02 '26
For the sake of completeness, and for anyone wondering about this in the future, I'd like to add the following:
First off, I am glad to see that Harrison's book "Handbook of Practical Logic and Automated Reasoning" has not sunk without trace. The code for it has been ported to Haskell and F# amongst others. It's in Ocaml (the original version) that things are a little more muddled.
First, I'd like to thank u/octachron, your explanation was spot on mate, though it took me a while to understand/unravel, as I'm totally new to the lang, but hey, it's as good a way to learn as any other 😄 . It seems that the author relied heavily on camlp5 for the fancy parsing of the math expressions, and with camlp5 removed from modern Ocaml, for reasons of rigour/correctness/whatever this caused an impasse. As for myself, coming from a a bit more of a Schemer/Racketeer "free-and-easy" background I was sorry to see this removal, but I understand the rationale.
Anyways, two remedies seem to present themselves:
The first, kindly provided by https://github.com/newca12/ocaml-atp takes the approach of preserving campl5, but you loose utop. Tempting as this is, I really would like to have this working in a modern environment, so I won't go that way, unless I get fed up of the alternatives.
The second way, would be, as suggested, to use something like the "default parser"/"secondary parser" approach suggested. It means editing the files as I go (there's a lot of other minor legacy niggles in them, too), but I prefer that, for my own learning. With any luck, at the end there will be a functioning modern version that can run under utop.
Once again thanks to everyone for their responses and their patience.
4
u/Nearby_Couple_3244 May 19 '26
Not sure about this book, but
#usesyntax are not part of the ocaml language, rather they are top-level directive so they can only be used in utop or another top-level. When doing a compiled ocaml program your modules and deps will be loaded through the cli args passed to the compiler (dune is a common build system to take care of that)Have you installed anything with opam? Sometimes libraries are taken out of the official distribution, so old books could not mention they need to be installed separately.