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'。然後我看了看自述文件，發現我可以用'源數據庫'來代替，而這會爲我做所有事情。 –