[ ソース: coq ]
パッケージ: coq (8.3.pl4+dfsg-1 など)
coq に関するリンク
Debian の資源:
coq ソースパッケージをダウンロード:
メンテナ:
- Debian OCaml Maintainers (QA ページ, メールアーカイブ)
- Ralf Treinen (QA ページ)
- Samuel Mimram (QA ページ)
- Stéphane Glondu (QA ページ)
外部の資源:
- ホームページ [coq.inria.fr]
類似のパッケージ:
高階述語論理証明アシスタント (トップレベルおよびコンパイラ)
Coq は高階述語論理の証明アシスタントで、コンピュータプログラムを形式的な仕 様との整合性を保ちながら開発できます。Objective Caml と Camlp5 を用いて開発 されています。
本パッケージは Coq へのコマンドラインインターフェース coqtop を提供します。
Coq のグラフィカルインターフェースは coqide パッケージが提供します。 Coq は ProofGeneral とも併用でき、証明を emacs や xemacs で編集できるように なります。これには proofgeneral パッケージのインストールが必要です。
その他の coq 関連パッケージ
|
|
|
-
- dep: coq-libs (= 8.1.pl3+dfsg-1) [m68k]
- パッケージは利用できません
-
- dep: coq-theories (= 8.2.pl2+dfsg-2) [hppa, powerpcspe]
- 高階論理用の証明アシスタント (理論)
- dep: coq-theories (= 8.3.pl2+dfsg-1) [sparc64]
- dep: coq-theories (= 8.3.pl4+dfsg-1) [hppa, m68k, powerpcspe, sparc64 以外]
-
- dep: emacsen-common
- 全 Emacsen 用の共通機能
-
- dep: libc0.1 (>= 2.7) [kfreebsd-amd64, kfreebsd-i386]
- 組込用 GNU C ライブラリ: 共有ライブラリ
以下のパッケージによって提供される仮想パッケージでもあります: libc0.1-udeb
-
- dep: libc0.3 (>= 2.7) [hurd-i386]
- 組込用 GNU C ライブラリ: 共有ライブラリ
以下のパッケージによって提供される仮想パッケージでもあります: libc0.3-udeb
-
- dep: libc6 (>= 2.11) [powerpcspe]
- 組込用 GNU C ライブラリ: 共有ライブラリ
以下のパッケージによって提供される仮想パッケージでもあります: libc6-udeb
- dep: libc6 (>= 2.2) [hppa]
- dep: libc6 (>= 2.5-5) [m68k]
- dep: libc6 (>= 2.7) [amd64, armel, i386, powerpc, sparc]
-
- dep: libcoq-ocaml-ehg05 [armel]
- 以下のパッケージによって提供される仮想パッケージです: libcoq-ocaml
-
- dep: libcoq-ocaml-m0xl3 [amd64, kfreebsd-amd64]
- 以下のパッケージによって提供される仮想パッケージです: libcoq-ocaml
-
- dep: libcoq-ocaml-nc3h8 [alpha, armhf, ia64, mips, mipsel, s390, s390x, sh4]
- 以下のパッケージによって提供される仮想パッケージです: libcoq-ocaml
-
- dep: libcoq-ocaml-rn5x5 [sparc64]
- 以下のパッケージによって提供される仮想パッケージです: libcoq-ocaml
-
- dep: libcoq-ocaml-s00f5 [hurd-i386, i386, kfreebsd-i386, powerpc, sparc]
- 以下のパッケージによって提供される仮想パッケージです: libcoq-ocaml
-
- dep: libgcc1 (>= 1:4.4.0) [armel]
- GCC 共有ライブラリ
-
- dep: libncurses5 (>= 5.6+20071006-3) [m68k]
- 端末処理用共有ライブラリ
-
- dep: ocaml-base-nox-3.10.2 [m68k]
- パッケージは利用できません
-
- dep: ocaml-base-nox-3.11.2 [hppa, powerpcspe]
- 以下のパッケージによって提供される仮想パッケージです: ocaml-base-nox
-
- dep: ocaml-base-nox-3.12.0 [sparc64]
- 以下のパッケージによって提供される仮想パッケージです: ocaml-base-nox
-
- dep: ocaml-base-nox-3.12.1 [hppa, m68k, powerpcspe, sparc64 以外]
- 以下のパッケージによって提供される仮想パッケージです: ocaml-base-nox
-
- dep: tex-common (>= 1.10) [m68k]
- common infrastructure for building and installing TeX
-
- rec: coqide [hppa, m68k, powerpcspe, sparc64 以外]
- 高階論理用証明アシスタント (gtk インターフェイス)
- または proofgeneral
- generic frontend for proof assistants
-
- rec: coqide [hppa, m68k, powerpcspe, sparc64]
- 高階論理用証明アシスタント (gtk インターフェイス)
- または proofgeneral-coq
- 証明アシスタント用の汎用インターフェイス - coq サポート
-
- sug: cle [m68k]
- パッケージは利用できません
-
- sug: coq-doc
- documentation for Coq
-
- sug: ledit [m68k]
- 対話的プログラム向けのラインエディタ
-
- sug: ledit [m68k 以外]
- 対話的プログラム向けのラインエディタ
- または readline-editor
- 以下のパッケージによって提供される仮想パッケージです: ledit, rlfe, rlwrap
-
- sug: libcoq-ocaml-dev [m68k 以外]
- development libraries and tools for Coq
-
- sug: ocaml-nox [m68k 以外]
- クラスベースのオブジェクトシステムを持った ML 言語の実装
- sug: ocaml-nox (>= 3.08) [m68k]
-
- sug: proofgeneral [hppa, m68k, powerpcspe, sparc64 以外]
- generic frontend for proof assistants
-
- sug: proofgeneral-coq [hppa, m68k, powerpcspe, sparc64]
- 証明アシスタント用の汎用インターフェイス - coq サポート
-
- sug: why (>= 2.19) [m68k 以外]
- Software verification tool
coq のダウンロード
| アーキテクチャ | バージョン | パッケージサイズ | インストールサイズ | ファイル |
|---|---|---|---|---|
| alpha (非公式の移植版) | 8.3.pl4+dfsg-1 | 1,769.9 kB | 8,225.0 kB | [ファイル一覧] |
| amd64 | 8.3.pl4+dfsg-1 | 5,542.9 kB | 18,432.0 kB | [ファイル一覧] |
| armel | 8.3.pl4+dfsg-1 | 5,967.2 kB | 17,898.0 kB | [ファイル一覧] |
| armhf | 8.3.pl4+dfsg-1 | 1,770.7 kB | 8,225.0 kB | [ファイル一覧] |
| hppa | 8.2.pl2+dfsg-2 | 3,608.8 kB | 18,268.0 kB | [ファイル一覧] |
| hurd-i386 | 8.3.pl4+dfsg-1+b1 | 4,941.7 kB | 15,044.0 kB | [ファイル一覧] |
| i386 | 8.3.pl4+dfsg-1 | 4,946.3 kB | 15,045.0 kB | [ファイル一覧] |
| ia64 | 8.3.pl4+dfsg-1+b1 | 1,770.0 kB | 8,225.0 kB | [ファイル一覧] |
| kfreebsd-amd64 | 8.3.pl4+dfsg-1 | 5,537.4 kB | 18,311.0 kB | [ファイル一覧] |
| kfreebsd-i386 | 8.3.pl4+dfsg-1 | 4,940.5 kB | 14,925.0 kB | [ファイル一覧] |
| m68k (非公式の移植版) | 8.1.pl3+dfsg-1+b2 | 4,014.9 kB | 18,580.0 kB | [ファイル一覧] |
| mips | 8.3.pl4+dfsg-1 | 1,768.9 kB | 8,225.0 kB | [ファイル一覧] |
| mipsel | 8.3.pl4+dfsg-1+b1 | 1,768.6 kB | 8,225.0 kB | [ファイル一覧] |
| powerpc | 8.3.pl4+dfsg-1 | 5,427.1 kB | 15,876.0 kB | [ファイル一覧] |
| powerpcspe (非公式の移植版) | 8.2.pl2+dfsg-2 | 3,606.8 kB | 18,260.0 kB | [ファイル一覧] |
| s390 | 8.3.pl4+dfsg-1 | 1,770.0 kB | 8,225.0 kB | [ファイル一覧] |
| s390x | 8.3.pl4+dfsg-1 | 1,771.4 kB | 8,225.0 kB | [ファイル一覧] |
| sh4 (非公式の移植版) | 8.3.pl4+dfsg-1 | 1,770.3 kB | 8,225.0 kB | [ファイル一覧] |
| sparc | 8.3.pl4+dfsg-1 | 5,289.9 kB | 15,807.0 kB | [ファイル一覧] |
| sparc64 (非公式の移植版) | 8.3.pl2+dfsg-1 | 1,763.2 kB | 8,432.0 kB | [ファイル一覧] |