Пакунок: coq (8.20.1+dfsg-1 and others)

[ Source: coq  ]

Інтерактивний програмний засіб доведення теорем для логіки вищого порядку (інтерактивне середовище і компілятор)

Coq — допоміжний інструмент для доведення теорем логіки вищого порядку, що дозволяє розробляти комп'ютерні програми відповідно до їх формальної специфікації. Ця програма написана на Objective Caml та Camlp5.

Пакунок надає „coqtop“, інтерфейс командного рядка для Coq.

Графічний інтерфейс Coq надається пакунком „coqide“. Coq також може використовуватися з ProofGeneral, який дозволяє редагувати докази в „emacs“ та „xemacs“. Останнє вимагає встановлення пакунка „proofgeneral“.

Tags: Software Development: Compiler, Field: Математика, Implemented in: implemented-in::ocaml, interface::commandline, User Interface: Text-based Interactive, Role: role::program, scope::utility, Interface Toolkit: Ncurses TUI

Інші пакунки пов'язані з coq

• dep: coq-libs (= 8.1.pl3+dfsg-1) [m68k]

  Пакунок недоступний

• dep: coq-theories (= 8.12.0-3+b3) [alpha, hppa, ia64, sh4, sparc64, x32]

  proof assistant for higher-order logic (theories)

• dep: emacsen-common [m68k]

  Спільні засоби для усіх пакунків Emacs

• dep: libc6 (>= 2.38) [amd64, arm64, ppc64, ppc64el, riscv64, s390x]

  Бібліотека GNU C: спільні бібліотеки
  also a virtual package provided by libc6-udeb

  dep: libc6 (>= 2.5-5) [m68k]

• dep: libcoq-core-ocaml-7yf86 [s390x]

  virtual package provided by libcoq-core-ocaml

• dep: libcoq-core-ocaml-ajzi5 [arm64]

  virtual package provided by libcoq-core-ocaml

• dep: libcoq-core-ocaml-at3u5 [amd64]

  virtual package provided by libcoq-core-ocaml

• dep: libcoq-core-ocaml-k4nx1 [ppc64el]

  virtual package provided by libcoq-core-ocaml

• dep: libcoq-core-ocaml-t2147 [riscv64]

  virtual package provided by libcoq-core-ocaml

• dep: libcoq-core-ocaml-yi844 [ppc64]

  virtual package provided by libcoq-core-ocaml

• dep: libcoq-ocaml-4s3g2 [alpha, hppa, ia64, sh4, sparc64, x32]

  virtual package provided by libcoq-ocaml

• dep: libcoq-stdlib (= 8.19.1+dfsg-3) [ppc64]

  proof assistant for higher-order logic (theories)

  dep: libcoq-stdlib (= 8.20.1+dfsg-1) [amd64, arm64, ppc64el, riscv64, s390x]

• dep: libfindlib-ocaml-5dit4 [arm64]

  virtual package provided by libfindlib-ocaml

• dep: libfindlib-ocaml-9a346 [s390x]

  virtual package provided by libfindlib-ocaml

• dep: libfindlib-ocaml-l8hb7 [ppc64]

  Пакунок недоступний

• dep: libfindlib-ocaml-o8mp7 [ppc64el]

  virtual package provided by libfindlib-ocaml

• dep: libfindlib-ocaml-t4zk4 [riscv64]

  virtual package provided by libfindlib-ocaml

• dep: libfindlib-ocaml-xdxk1 [amd64]

  virtual package provided by libfindlib-ocaml

• dep: libgmp10 (>= 2:6.3.0+dfsg) [amd64, arm64, ppc64, ppc64el, riscv64, s390x]

  Арифметична бібліотека багатоточності

• dep: libncurses5 (>= 5.6+20071006-3) [m68k]

  Пакунок недоступний

• dep: libnum-ocaml-3st20 [alpha, hppa, ia64, sh4, sparc64, x32]

  virtual package provided by libnum-ocaml

• dep: libstdlib-ocaml-fxjy5 [amd64, arm64, ppc64el, riscv64]

  virtual package provided by libstdlib-ocaml

• dep: libstdlib-ocaml-gats1 [ppc64]

  Пакунок недоступний

• dep: libstdlib-ocaml-ke4j9 [s390x]

  virtual package provided by libstdlib-ocaml

• dep: libzarith-ocaml-avzf2 [ppc64]

  Пакунок недоступний

• dep: libzarith-ocaml-f1se9 [amd64, arm64, ppc64el, riscv64]

  virtual package provided by libzarith-ocaml

• dep: libzarith-ocaml-i2hh0 [s390x]

  virtual package provided by libzarith-ocaml

• dep: ocaml [amd64, arm64, ppc64, ppc64el, riscv64, s390x]

  ML language implementation with a class-based object system

• dep: ocaml-base-4.14.1 [ppc64]

  virtual package provided by ocaml-base

• dep: ocaml-base-5.3.0 [amd64, arm64, ppc64el, riscv64, s390x]

  virtual package provided by ocaml-base

• dep: ocaml-base-nox-3.10.2 [m68k]

  Пакунок недоступний

• dep: ocaml-base-nox-4.11.1 [alpha, hppa, ia64, sh4, sparc64, x32]

  Пакунок недоступний

• dep: ocaml-findlib [not m68k]

  management tool for OCaml libraries

• dep: ocaml-nox [alpha, hppa, ia64, sh4, sparc64, x32]

  transitional package for ocaml

• dep: python3 [not m68k]

  interactive high-level object-oriented language (default python3 version)

• dep: tex-common (>= 1.10) [m68k]

  Загальна інфраструктура для побудови та встановлення TeX

• rec: coqide

  proof assistant for higher-order logic (gtk interface)

  or proofgeneral-coq

  Пакунок недоступний

• sug: cle [m68k]

  Пакунок недоступний

• sug: coq-doc

  documentation for Coq

• sug: coqide [not m68k]

  proof assistant for higher-order logic (gtk interface)

  or proofgeneral

  generic frontend for proof assistants

• sug: ledit [m68k]

  line editor for interactive programs

• sug: ledit [not m68k]

  line editor for interactive programs

  or readline-editor

  virtual package provided by ledit, rlfe, rlwrap

• sug: libcoq-core-ocaml-dev [amd64, arm64, ppc64, ppc64el, riscv64, s390x]

  development libraries and tools for Coq

• sug: libcoq-ocaml-dev [alpha, hppa, ia64, sh4, sparc64, x32]

  development libraries and tools for Coq

• sug: ocaml-nox (>= 3.08) [m68k]

  transitional package for ocaml

• sug: proofgeneral-coq [m68k]

  Пакунок недоступний

• sug: why (>= 2.19) [not m68k]

  Пакунок недоступний

Завантажити coq

Завантаження для всіх доступних архітектур

Архітектура	Версія	Розмір пакунка	Розмір після встановлення	Файли
alpha (unofficial port)	8.12.0-3+b3	103,380.6 kB	412,882.0 kB	[список файлів]
amd64	8.20.1+dfsg-1	68,574.8 kB	255,831.0 kB	[список файлів]
arm64	8.20.1+dfsg-1	72,692.7 kB	277,363.0 kB	[список файлів]
hppa (unofficial port)	8.12.0-3+b3	103,393.2 kB	412,952.0 kB	[список файлів]
ia64 (unofficial port)	8.12.0-3+b3	103,379.1 kB	412,878.0 kB	[список файлів]
m68k (unofficial port)	8.1.pl3+dfsg-1+b2	4,014.9 kB	18,580.0 kB	[список файлів]
ppc64 (unofficial port)	8.19.1+dfsg-3	80,065.5 kB	339,636.0 kB	[список файлів]
ppc64el	8.20.1+dfsg-1	69,187.4 kB	266,936.0 kB	[список файлів]
riscv64	8.20.1+dfsg-1	69,527.1 kB	266,346.0 kB	[список файлів]
s390x	8.20.1+dfsg-1	69,405.7 kB	274,877.0 kB	[список файлів]
sh4 (unofficial port)	8.12.0-3+b3	103,401.4 kB	412,954.0 kB	[список файлів]
sparc64 (unofficial port)	8.12.0-3+b3	103,374.8 kB	412,882.0 kB	[список файлів]
x32 (unofficial port)	8.12.0-3+b3	103,397.8 kB	412,954.0 kB	[список файлів]