[ ソース: coq ]
パッケージ: coq (8.4~beta+dfsg-4 など)
coq に関するリンク
Debian の資源:
coq ソースパッケージをダウンロード:
メンテナ:
- Debian OCaml Maintainers (QA ページ, メールアーカイブ)
- Ralf Treinen (QA ページ)
- Samuel Mimram (QA ページ)
- Stéphane Glondu (QA ページ)
外部の資源:
- ホームページ [coq.inria.fr]
類似のパッケージ:
試験的な (experimental の) パッケージ
警告: このパッケージは experimental ディストリビューションのものです。つまり、おそらく不安定でバグがあり、それどころかデータの損失を起こすかもしれません。使用前には、変更履歴やその他の参照可能なドキュメントを必ず調べてください。
高階述語論理証明アシスタント (トップレベルおよびコンパイラ)
Coq は高階述語論理の証明アシスタントで、コンピュータプログラムを形式的な仕 様との整合性を保ちながら開発できます。Objective Caml と Camlp5 を用いて開発 されています。
本パッケージは Coq へのコマンドラインインターフェース coqtop を提供します。
Coq のグラフィカルインターフェースは coqide パッケージが提供します。 Coq は ProofGeneral とも併用でき、証明を emacs や xemacs で編集できるように なります。これには proofgeneral パッケージのインストールが必要です。
その他の coq 関連パッケージ
|
|
|
-
- dep: coq-theories (= 8.4~beta+dfsg-3) [alpha, sh4]
- 高階論理用の証明アシスタント (理論)
- dep: coq-theories (= 8.4~beta+dfsg-4) [alpha, sh4 以外]
-
- dep: emacsen-common
- 全 Emacsen 用の共通機能
-
- dep: libc0.1 (>= 2.7) [kfreebsd-amd64, kfreebsd-i386]
- 組込用 GNU C ライブラリ: 共有ライブラリ
以下のパッケージによって提供される仮想パッケージでもあります: libc0.1-udeb
-
- dep: libc6 (>= 2.7) [amd64, armel, i386, powerpc, sparc]
- 組込用 GNU C ライブラリ: 共有ライブラリ
以下のパッケージによって提供される仮想パッケージでもあります: libc6-udeb
-
- dep: libcoq-ocaml-4l581 [i386, kfreebsd-i386, powerpc, sparc]
- 以下のパッケージによって提供される仮想パッケージです: libcoq-ocaml
-
- dep: libcoq-ocaml-5q2v9 [armhf, ia64, mips, mipsel, s390, s390x]
- 以下のパッケージによって提供される仮想パッケージです: libcoq-ocaml
-
- dep: libcoq-ocaml-b8s62 [amd64, kfreebsd-amd64]
- 以下のパッケージによって提供される仮想パッケージです: libcoq-ocaml
-
- dep: libcoq-ocaml-sg318 [armel]
- 以下のパッケージによって提供される仮想パッケージです: libcoq-ocaml
-
- dep: libcoq-ocaml-unb18 [alpha, sh4]
- 以下のパッケージによって提供される仮想パッケージです: libcoq-ocaml
-
- dep: libgcc1 (>= 1:4.4.0) [armel]
- GCC 共有ライブラリ
-
- dep: ocaml-base-nox-3.12.1
- パッケージは利用できません
-
- rec: coqide
- 高階論理用証明アシスタント (gtk インターフェイス)
- または proofgeneral
- generic frontend for proof assistants
-
- sug: coq-doc
- documentation for Coq
-
- sug: ledit
- 対話的プログラム向けのラインエディタ
- または readline-editor
- パッケージは利用できません
-
- sug: libcoq-ocaml-dev
- development libraries and tools for Coq
-
- sug: ocaml-nox
- クラスベースのオブジェクトシステムを持った ML 言語の実装
-
- sug: proofgeneral
- generic frontend for proof assistants
-
- sug: why (>= 2.19)
- Software verification tool
coq のダウンロード
| アーキテクチャ | バージョン | パッケージサイズ | インストールサイズ | ファイル |
|---|---|---|---|---|
| alpha (非公式の移植版) | 8.4~beta+dfsg-3 | 1,867.2 kB | 8,689.0 kB | [ファイル一覧] |
| amd64 | 8.4~beta+dfsg-4 | 5,835.7 kB | 19,338.0 kB | [ファイル一覧] |
| armel | 8.4~beta+dfsg-4 | 6,333.6 kB | 18,969.0 kB | [ファイル一覧] |
| armhf | 8.4~beta+dfsg-4 | 1,868.0 kB | 8,699.0 kB | [ファイル一覧] |
| i386 | 8.4~beta+dfsg-4 | 5,178.5 kB | 15,712.0 kB | [ファイル一覧] |
| ia64 | 8.4~beta+dfsg-4 | 1,867.4 kB | 8,570.0 kB | [ファイル一覧] |
| kfreebsd-amd64 | 8.4~beta+dfsg-4 | 5,834.2 kB | 19,219.0 kB | [ファイル一覧] |
| kfreebsd-i386 | 8.4~beta+dfsg-4 | 5,173.5 kB | 15,594.0 kB | [ファイル一覧] |
| mips | 8.4~beta+dfsg-4 | 1,870.8 kB | 8,699.0 kB | [ファイル一覧] |
| mipsel | 8.4~beta+dfsg-4 | 1,869.1 kB | 8,699.0 kB | [ファイル一覧] |
| powerpc | 8.4~beta+dfsg-4 | 5,699.2 kB | 16,604.0 kB | [ファイル一覧] |
| s390 | 8.4~beta+dfsg-4 | 1,867.3 kB | 8,699.0 kB | [ファイル一覧] |
| s390x | 8.4~beta+dfsg-4 | 1,867.6 kB | 8,699.0 kB | [ファイル一覧] |
| sh4 (非公式の移植版) | 8.4~beta+dfsg-3 | 1,867.9 kB | 8,689.0 kB | [ファイル一覧] |
| sparc | 8.4~beta+dfsg-4 | 5,550.2 kB | 16,550.0 kB | [ファイル一覧] |
