Utop vs OCaml interpreter module loads

Learning
1

I am pretty new to OCaml. I am working through John Harrison’s “Practical Logic and Automated Reasoning” book, which provides source code in OCaml that you can download and use to assist you with reading the book. I find that his << & >> quotation mark parser works in the ‘ocaml’ interpreter but fails in the ‘utop’ interpreter, even though the source that he provides to initialise his functions seems to load error-free in both, via use “init.ml”;; & “intro.ml”. I feel that ‘utop’ fails because some module is missing that is provided under ‘ocaml’.

My question is, how can I display all loaded modules within the interpreter so that I can compare ‘utop’/‘ocaml’ side by side, to see what missing library is preventing proper parsing in ‘utop’.

Thank you for your help.

2

It’s hard to guess if you don’t link to the .ml files you’re talking about…
I believe it is the ones linked from this page?: https://www.cl.cam.ac.uk/~jrh13/atp/ (init.ml, intro.ml).

The issue might be that init.ml is trying to load camlp5 in a way that doesn’t please utop. Maybe try using this init.ml instead (after you make sure that you have installed camlp5):

#load "nums.cma";;                                     (* For Ocaml 3.06     *)
#require "camlp5";;

type dummy_interactive = START_INTERACTIVE | END_INTERACTIVE;;
#use "initialization.ml";;
#use "Quotexpander.ml";;
#use "atp_interactive.ml";;
1 Like