在ocamldebug中来自ocamltop的`#use`指令是否等效？
在ocamltop中(加载我的文件之后)，我可以运行以下命令
#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的目录结构。)
回答 1
Stack Overflow用户
发布于 2013-09-29 15:01:46
似乎你试图在ocamldebug中使用toplevel指令(以#开头的行)，而ocamldebug对这些指令一无所知。您必须使用调试器命令与ocamldebug对话，有关详细信息，请参阅ocamldebug documentation.
加载和安装打印机如下所示：
directory dependencies
load_printer "printers.cmo"
install_printer Printers.pp_thing请注意显式的模块名称-没有#use和open。还要注意，ocamldebug将在其目录列表中搜索printers.cmo的依赖项。如果出现未定义的全局错误，则可能需要向该列表中添加一些条目。
一旦一切正常，你就不会想再输入那些垃圾了。将其全部放入一个文件中，并使用printers.debug命令加载该文件：
source printers.debughttps://stackoverflow.com/questions/19047058
复制相似问题
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号