Language

Package: proof-general @ 4.4-1.1b1083e

Synopsis

Generic front-end for proof assistants based on Emacs

Description

Proof General is a major mode to turn Emacs into an interactive proof assistant to write formal mathematical proofs using a variety of theorem provers.

Home page
https://proofgeneral.github.io/
Location
gnu/packages/coq.scm (line: 148, column: 4)
License

Derivations

SystemTargetDerivationBuild status
x86_64-linux/gnu/store/nb1nc43zm89fhh6dlbmc0si07qz23pjw-proof-general-4.4-1.1b1083e.drv
x86_64-linuxx86_64-w64-mingw32/gnu/store/ngi0jhzqcgypdsrvi5bxypfwrf0p7s8f-proof-general-4.4-1.1b1083e.drv
x86_64-linuxriscv64-linux-gnu/gnu/store/jn98snxsrqk5kl45dpjj4kb459mvp14x-proof-general-4.4-1.1b1083e.drv
x86_64-linuxpowerpc-linux-gnu/gnu/store/djwhcwv7n04dhzprwjysw17bw1k3250q-proof-general-4.4-1.1b1083e.drv
x86_64-linuxpowerpc64le-linux-gnu/gnu/store/n2rfh17xfwhrmi4mlvflaki6r1nql8dg-proof-general-4.4-1.1b1083e.drv
x86_64-linuxmips64el-linux-gnu/gnu/store/wf3x7la4i5qqglycr8n40kazpywdj40c-proof-general-4.4-1.1b1083e.drv
x86_64-linuxi686-w64-mingw32/gnu/store/wjpjqr1v65kyjj6mlj8xxkfvq7l5kbn8-proof-general-4.4-1.1b1083e.drv
x86_64-linuxi586-pc-gnu/gnu/store/r1h6vm2jzs8994pskq21w425kwbvchwz-proof-general-4.4-1.1b1083e.drv
x86_64-linuxarm-linux-gnueabihf/gnu/store/fb3zlmp4w6wilmq06w08qajsqinnphc3-proof-general-4.4-1.1b1083e.drv
x86_64-linuxaarch64-linux-gnu/gnu/store/wc2i17n0b4iidw5bhj03j39gx49rhk2j-proof-general-4.4-1.1b1083e.drv
riscv64-linux/gnu/store/3x4rqgi9qc1hqmdrn6kv0hklrmba4gxr-proof-general-4.4-1.1b1083e.drv
    powerpc-linux/gnu/store/jn5b1is1p57m6n1qgrlmjry4qha6flhd-proof-general-4.4-1.1b1083e.drv
      powerpc64le-linux/gnu/store/a0sfhs4kvwsh5y1dhgd1bzc4iyjiyy8x-proof-general-4.4-1.1b1083e.drv
      mips64el-linux/gnu/store/a323mbqn0775pw6f6jaa1al2gr1r6nlc-proof-general-4.4-1.1b1083e.drv
        i686-linux/gnu/store/mg2j1q47zwq0ndawbsr6x8im713hzb59-proof-general-4.4-1.1b1083e.drv
        i586-gnu/gnu/store/hcf18ddxglci5815ls6g9iqgr0k8s005-proof-general-4.4-1.1b1083e.drv
        armhf-linux/gnu/store/abfm4k65vl16zwrml6wxvpjisl0swkdj-proof-general-4.4-1.1b1083e.drv
        aarch64-linux/gnu/store/vavyc6xk17jxdcqyx1q0fa1aryxf15j5-proof-general-4.4-1.1b1083e.drv

        Lint warnings

        LinterMessageLocation
        input-labels

        Identify input labels that do not match package names

        label 'emacs' does not match package name 'emacs-minimal'
        derivation

        Report failure to compile a package to a derivation

        failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7f8ed7409c60> input: ("_" "static")>
        derivation

        Report failure to compile a package to a derivation

        failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7fa7aa068c60> input: ("_" "static")>
        derivation

        Report failure to compile a package to a derivation

        failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7f5755cb9c60> input: ("_" "static")>
        derivation

        Report failure to compile a package to a derivation

        failed to create i586-gnu derivation: #<&package-input-error package: #<package nghttp2@1.48.0 gnu/packages/web.scm:7487 7f119da52c60> input: ("_" "static")>