는 (내 파일을로드 한 후), 나는 다음과 같은 명령 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입니다.)
나는 가까이에 있다고 생각합니다. 'Pp'는 camlp4/5가 아닌'lib /'아래의'coq' 배포판에 있습니다. - 그 디렉토리를 포함하려는 의도라고 가정하고 있습니까? – nlucaroni
예. 그리고 내가 처음으로 정의되지 않은 전역으로 체인을 추적했을 때'load_printer str'이 필요했습니다. 그리고 README를 보았습니다. 대신에'소스 db '를 사용할 수 있다는 것을 알게되었습니다. 그러면 저를 위해 모든 것을 할 수 있습니다. –