2013-09-27 1 views
0

는 (내 파일을로드 한 후), 나는 다음과 같은 명령 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입니다.)

+0

나는 가까이에 있다고 생각합니다. 'Pp'는 camlp4/5가 아닌'lib /'아래의'coq' 배포판에 있습니다. - 그 디렉토리를 포함하려는 의도라고 가정하고 있습니까? – nlucaroni

+0

예. 그리고 내가 처음으로 정의되지 않은 전역으로 체인을 추적했을 때'load_printer str'이 필요했습니다. 그리고 README를 보았습니다. 대신에'소스 db '를 사용할 수 있다는 것을 알게되었습니다. 그러면 저를 위해 모든 것을 할 수 있습니다. –

답변

0

ocamldebug에서 최상위 지시문 (#으로 시작하는 줄)을 사용하려는 것 같습니다.이 경우에 대해서는 알지 못합니다. 아니오 #use과도 없다 -

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

참고 명시 적 모듈 이름 : 당신은 ocamldebug documentation.

로드 및 프린터를 설치하는 다음과 같이 보입니다를 볼 수있는 내용은, 디버거 명령을 사용하여 ocamldebug 할 말을해야 open. 또한 ocamldebug는 종속성이 printers.cmo 인 디렉토리 목록을 검색합니다. 정의되지 않은 전역 오류가 발생하면 해당 목록에 일부 항목을 추가해야 할 수 있습니다.

모든 것이 작동하면 모든 정크를 다시 입력하지 않아도됩니다. 파일에 모두 넣으십시오 (예 : printers.debug). 소스 명령을 사용하여로드하십시오.

관련 문제