0
在ocamltop（我加载文件之后），我可以运行下面的命令相当于从ocamldebug ocamltop`＃use`指令？
#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>
但我不能跟踪未导出的函数，所以我想通过功能与ocamldebug步骤来代替。但是，当我尝试打印我想要看到的内容时，我收到了诸如f : Term.constr = <abstr>之类的内容。所以我想从include文件来安装打印机，它与
#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;;
和base_include开始看起来大约像
#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
...
所以在ocamldebug，我尝试
(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'
所以我如何加载这些打印机。 （仅供参考，目录结构为https://github.com/HoTT/coq。）
我想你靠近。 'Pp'位于下'coq'分布'的lib /'，而不是在camlp4/5 - 我很假设是，包括这些目录的意图是什么？ – nlucaroni
是的。当我追踪链备份到第一未定义的全局，我最终需要为'load_printer str'。然后我看了看自述文件，发现我可以用'源数据库'来代替，而这会为我做所有事情。 –