Ito ang command coqdep na maaaring patakbuhin sa OnWorks na libreng hosting provider gamit ang isa sa aming maramihang libreng online na workstation gaya ng Ubuntu Online, Fedora Online, Windows online emulator o MAC OS online emulator
PROGRAMA:
NAME
coqdep - Compute inter-module dependencies para sa Coq at Caml programs
SINOPSIS
coqdep [ -w ] [ -I direktoryo ] [ -coqlib direktoryo ] [ -c ] [ -i ] [ -D ] [ -slash ]
filename ... direktoryo ...
DESCRIPTION
coqdep kalkulahin ang inter-module dependencies para sa Coq at Caml programs, at ini-print ang
dependencies sa karaniwang output sa isang format na nababasa ng make. Kapag ang isang direktoryo ay
ibinigay bilang argumento, ito ay recursively tumingin sa.
Ang mga dependency ng mga module ng Coq ay nakalkula sa pamamagitan ng pagtingin sa Mangailangan mga utos (Require, Require
I-export, Mangailangan ng Pag-import), Magpahayag ML Module mga utos at Load mga utos. Dependencies
kaugnay sa mga module mula sa Coq library ay hindi naka-print.
Ang mga dependency ng Caml modules ay nakalkula sa pamamagitan ng pagtingin sa buksan mga direktiba at ang tuldok
notasyon module.value.
Opsyon
-c Nagpi-print ng mga dependency ng Caml modules. (Sa mga module ng Caml, ang pag-uugali ay
eksaktong kapareho ng ocamldep).
-w Nagpi-print ng babala kung isang Coq command Magpahayag ML Module ay mali. (Halimbawa,
sinulat mo ang `Declare ML Module "A".', ngunit ang module A ay naglalaman ng #open "B"). Ang
tamang command ay naka-print (tingnan ang opsyon -D). Ang babala ay nakalimbag sa pamantayan
error.
-D Hinahanap ng command na ito ang bawat command Magpahayag ML Module ng bawat Coq file na ibinigay bilang
argumento at kumpletuhin (kung kinakailangan) ang listahan ng mga module ng Caml. Ang bagong utos ay
naka-print sa karaniwang output. Walang dependency ang nakalkula sa opsyong ito.
-slash Nagpi-print ng mga path gamit ang isang slash sa halip na ang OS na partikular na separator. Ang pagpipiliang ito ay
kapaki-pakinabang kapag bumubuo sa ilalim ng Cygwin.
-I direktoryo
Ang mga file .v .ml .mli ng direktoryo direktoryo ay isinasaalang-alang sa panahon ng
calculus ng mga dependencies, ngunit ang kanilang sariling mga dependencies ay hindi naka-print.
-coqlib direktoryo
Isinasaad kung nasaan ang Coq library. Ang default na halaga ay natukoy sa
oras ng pag-install, at samakatuwid ang pagpipiliang ito ay hindi dapat gamitin sa ilalim ng normal
pangyayari.
Gumamit ng coqdep online gamit ang mga serbisyo ng onworks.net
