0

In ocamltop (after loading my file), I can run the following commands

#cd "/afs/csail.mit.edu/u/j/jgross/coq-HoTT/";;
#directory "/afs/csail.mit.edu/u/j/jgross/coq-HoTT/";;
#directory "/afs/csail.mit.edu/u/j/jgross/coq-HoTT/dev";;
#use "dev/include";;
#trace <some_function>

But I cannot trace functions which are not exported, so I'd like to step through functions with ocamldebug instead. However, when I try to print what I want to see, I get things like f : Term.constr = <abstr>. So I would like to install the printers from the include file., which starts with

#cd ".";;
#use "base_include";;

#install_printer  (* pp_stdcmds *) pppp;;

#install_printer  (* pattern *) pppattern;;
#install_printer  (* glob_constr *) ppglob_constr;;

#install_printer  (* constr *) ppconstr;;
#install_printer  (* constr_substituted *) ppsconstr;;

and base_include looks approximately like

#cd".";;
#directory "parsing";;
#directory "interp";;
...

#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
#directory "+camlp5";; (* Gramext is found in top_printers.ml *)

#use "top_printers.ml";;
#use "vm_printers.ml";;

#install_printer  (* identifier *) ppid;;
...

(* Open main files *)

open Names
open Term
open Typeops
open Term_typing
open Univ
...

So in ocamldebug, I try

(ocd) directory /afs/csail.mit.edu/u/j/jgross/coq-HoTT/
Directories : /afs/csail.mit.edu/u/j/jgross/coq-HoTT/ ...
(ocd) directory /afs/csail.mit.edu/u/j/jgross/coq-HoTT/dev
Directories : /afs/csail.mit.edu/u/j/jgross/coq-HoTT/dev ...
(ocd) use /afs/csail.mit.edu/u/j/jgross/coq-HoTT/dev/include
Unknown command.
(ocd) source /afs/csail.mit.edu/u/j/jgross/coq-HoTT/dev/include
Syntax error.
(ocd) source "/afs/csail.mit.edu/u/j/jgross/coq-HoTT/dev/include"
Syntax error.
(ocd) load_printer /afs/csail.mit.edu/u/j/jgross/coq-HoTT/dev/include
Error during code loading: /afs/csail.mit.edu/u/j/jgross/coq-HoTT/dev/include is not a bytecode object file
(ocd) load_printer top_printers.ml
Error during code loading: /afs/csail.mit.edu/u/j/jgross/coq-HoTT/dev/top_printers.ml is not a bytecode object file
(ocd) load_printer top_printers
Cannot find file top_printers
(ocd) shell ls /afs/csail.mit.edu/u/j/jgross/coq-HoTT/dev/
base_db           dynlink.cmx        ocamldebug-coq             set_raw_db         vm_printers.cmi
base_include      dynlink.ml         ocamldebug-coq.template    TODO               vm_printers.cmo
db                dynlink.ml.d       ocamldoc                   tools              vm_printers.ml
db_printers.ml    dynlink.o          ocamlopt_shared_os5fix.sh  top_printers.cmi   vm_printers.ml.d
db_printers.ml.d  header             printers.cma               top_printers.cmo
doc               include            printers.mllib             top_printers.ml
dynlink.cmi       macosify_accel.sh  printers.mllib.d           top_printers.ml.d
dynlink.cmo       Makefile.oug       README                     v8-syntax
(ocd) load_printer top_printers.cmi
Error during code loading: /afs/csail.mit.edu/u/j/jgross/coq-HoTT/dev/top_printers.cmi is not a bytecode object file
(ocd) load_printer top_printers.cmo
Error during code loading: error while linking /afs/csail.mit.edu/u/j/jgross/coq-HoTT/dev/top_printers.cmo.
Reference to undefined global `Pp'
(ocd) directory +camlp5
...
(ocd) directory +camlp4
...
(ocd) load_printer top_printers.cmo
Error during code loading: error while linking /afs/csail.mit.edu/u/j/jgross/coq-HoTT/dev/top_printers.cmo.
Reference to undefined global `Pp'

So how do I load these printers. (For reference, the directory structure is that of https://github.com/HoTT/coq.)

4

1 回答 1

0

似乎您正在尝试#在 ocamldebug 中使用顶级指令（以 开头的行），它对此一无所知。您必须使用调试器命令与 ocamldebug 交谈，有关详细信息，请参阅ocamldebug 文档。

加载和安装打印机如下所示：

directory dependencies
load_printer "printers.cmo"
install_printer Printers.pp_thing

注意明确的模块名称——没有#use和没有open。另请注意，ocamldebug 将在其目录列表中搜索printers.cmo. 如果您收到未定义的全局错误，您可能需要在该列表中添加一些条目。

一旦一切正常，你就不想再输入所有的垃圾了。把它全部放在一个文件中，比如说printers.debug，然后用 source 命令加载它：

source printers.debug
于 2013-09-29T07:01:46.147 回答