jocamlmklib(1) [debian man page]
JOCAMLMKLIB(1) General Commands Manual JOCAMLMKLIB(1) NAME
jocamlmklib - generate libraries with mixed C / Caml code. SYNOPSIS
ocalmklib [options] files DESCRIPTION
The jocamlmklib command facilitates the construction of libraries containing both Caml code and C code, and usable both in static linking and dynamic linking modes. OPTIONS
-h, --help Show summary of options. -cclib lib C library passed to jocamlc -a or jocamlopt(1) -a only. -ccopt opt C option passed to jocamlc(1) -a or jocamlopt(1) -a only. -custom Disable dynamic loading. -dllpath dir Add dir to the run-time search path for DLLs. -I dir Add dir to the path searched for Caml object files. -failsafe Fall back to static linking if DLL construction failed. -ldopt opt C option passed to the shared linker only. -linkall Build Caml archive with link-all behavior. -llib Specify a dependent C library. -Ldir Add dir to the path searched for C libraries. -jocamlc cmd Use cmd in place of jocamlc(1). -jocamlopt cmd Use cmd in place of jocamlopt(1). -o name Generated Caml library is named name.cma or name.cmxa. -oc name Generated C library is named dllname.so or libname.a. -rpath dir Same as -dllpath dir. -Rdir Same as -rpath. -verbose Print commands before executing them. -Wl, -rpath dir Same as -dllpath dir. -Wl, -rpath -Wl dir Same as -dllpath dir. -Wl, -Rdir Same as -dllpath dir. -Fdir Specify a framework directory (MacOSX). -framework name Use framework name (MacOSX). SEE ALSO
jocamlc(1), jocamlopt(1). AUTHOR
This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>, for the Debian project (but may be used by others). August 19, 2004 JOCAMLMKLIB(1)
Check Out this Related Man Page
COQIDE(1) General Commands Manual COQIDE(1) NAME
coqide - The Coq Proof Assistant graphical interface SYNOPSIS
coqide [ options ] DESCRIPTION
coqtop is a gtk graphical interface for the Coq proof assistant. For command-line-oriented use of Coq, see coqide(1) ; for batch-oriented use of Coq, see coqc(1). OPTIONS
-h Show the complete list of options accepted by coqide. -I dir, -include dir Add directory dir in the include path. -R dir coqdir Recursively map physical dir to logical coqdir. -src Add source directories in the include path. -is f, -inputstate f Read state from f.coq. -nois Start with an empty state. -outputstate f Write state in file f.coq. -load-ml-object f Load ML object file f. -load-ml-source f Load ML file f. -l f, -load-vernac-source f Load Coq file f.v (Load f.). -lv f, -load-vernac-source-verbose f Load Coq file f.v (Load Verbose f.). -load-vernac-object f Load Coq object file f.vo. -require f Load Coq object file f.vo and import it (Require f.). -compile f Compile Coq file f.v (implies -batch). -compile-verbose f Verbosely compile Coq file f.v (implies -batch). -opt Run the native-code version of Coq or Coq_SearchIsos. -byte Run the bytecode version of Coq or Coq_SearchIsos. -where Print Coq's standard library location and exit. -v Print Coq version and exit. -q Skip loading of rcfile. -init-file f Set the rcfile to f. -user u Use the rcfile of user u. -batch Batch mode (exits just after arguments parsing). -boot Boot mode (implies -q and -batch). -emacs Tells Coq it is executed under Emacs. -dump-glob f Dump globalizations in file f (to be used by coqdoc(1)). -impredicative-set Set sort Set impredicative. -dont-load-proofs Don't load opaque proofs in memory. -xml Export XML files either to the hierarchy rooted in the directory COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset). SEE ALSO
coqc(1), coqtop(1), coq-tex(1), coqdep(1). The Coq Reference Manual, The Coq web site: http://coq.inria.fr, /usr/share/doc/coqide/FAQ. AUTHOR
This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>, for the Debian project (but may be used by others). July 16, 2004 COQIDE(1)