Language

Package: proof-general @ 4.5-2.d668946

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: 140, column: 4)
License

Derivations

SystemTargetDerivationBuild status
x86_64-linux/gnu/store/8fxgzd4sd12w6cw7cmynm3xkmhdy96h6-proof-general-4.5-2.d668946.drv
x86_64-linuxxtensa-ath9k-elf/gnu/store/3ikhfb1cq98sxm3c8rjkv27zgippjfii-proof-general-4.5-2.d668946.drv
    x86_64-linuxx86_64-w64-mingw32/gnu/store/7ih83c1bjpqyspr94ff91a1xb5nr7x6w-proof-general-4.5-2.d668946.drv
    x86_64-linuxx86_64-pc-gnu/gnu/store/3mba8adfp90ws1142r4a7ryrwqx6dcap-proof-general-4.5-2.d668946.drv
    x86_64-linuxx86_64-linux-gnux32/gnu/store/n2yif1cvhzsf85kqs1m53pgy8mflyn6g-proof-general-4.5-2.d668946.drv
      x86_64-linuxriscv64-linux-gnu/gnu/store/9xc3l9r5ggpvr44yli01dr0mdnrij8wk-proof-general-4.5-2.d668946.drv
      x86_64-linuxpowerpc-linux-gnu/gnu/store/csa7bfc7hwr8g3db3md91cc8w5r0ypgr-proof-general-4.5-2.d668946.drv
        x86_64-linuxpowerpc64-linux-gnu/gnu/store/p5x0vis75h97ymy84rz680d1qylq8fpb-proof-general-4.5-2.d668946.drv
          x86_64-linuxpowerpc64le-linux-gnu/gnu/store/677rqs6lpd3ayia2sxw4l2xn8ibavrw1-proof-general-4.5-2.d668946.drv
          x86_64-linuxor1k-elf/gnu/store/2fscbj1yhnznpl5b9hzw9zvjiydlyh7k-proof-general-4.5-2.d668946.drv
            x86_64-linuxmips64el-linux-gnu/gnu/store/51k6qv7g0wia3pfx77vxhlzwyns55swl-proof-general-4.5-2.d668946.drv
              x86_64-linuxloongarch64-linux-gnu/gnu/store/8i3imdwc93zgq303n3cvkdayg2dgglj2-proof-general-4.5-2.d668946.drv
              x86_64-linuxi686-w64-mingw32/gnu/store/00h4m5lnj96l6p0fyqvyh2lc4j3lcxxm-proof-general-4.5-2.d668946.drv
                x86_64-linuxi586-pc-gnu/gnu/store/lsq8w5vcp85nv25znlk7i7fvw17jil3f-proof-general-4.5-2.d668946.drv
                x86_64-linuxavr/gnu/store/qqmqlxsryzrd7plpksjnf95l2vhp38lx-proof-general-4.5-2.d668946.drv
                  x86_64-linuxarm-linux-gnueabihf/gnu/store/fh8sy2cl8c7a8rgzz503n37k0y5x343v-proof-general-4.5-2.d668946.drv
                  x86_64-linuxaarch64-linux-gnu/gnu/store/90fii8ml5k07jv98sdz2aqkzj8rr4v9j-proof-general-4.5-2.d668946.drv
                  x86_64-gnu/gnu/store/f6a77bqc5j0qhgpdwrl9mjskk42g6229-proof-general-4.5-2.d668946.drv
                    riscv64-linux/gnu/store/bch70kl4bnjwdfc7a09r47vs4yrqprnw-proof-general-4.5-2.d668946.drv
                    powerpc-linux/gnu/store/zjj052j522ny7v1jw3qdsnfwqsdxbcl6-proof-general-4.5-2.d668946.drv
                      powerpc64le-linux/gnu/store/xzk86zgv34bdgp9ri9hxdza2i3wspxpz-proof-general-4.5-2.d668946.drv
                      mips64el-linux/gnu/store/8p6468j9rjd00asjmy67mbxmp8fbn4sw-proof-general-4.5-2.d668946.drv
                        i686-linux/gnu/store/a74i5svki2qhqc1645chyz3pk0xiw7ky-proof-general-4.5-2.d668946.drv
                        i586-gnu/gnu/store/lhyg5h9asibnylx28njlhqaay3qvnia7-proof-general-4.5-2.d668946.drv
                          armhf-linux/gnu/store/lzk6i9fg01qgj7zn6qbxqhjlzgnz463i-proof-general-4.5-2.d668946.drv
                          aarch64-linux/gnu/store/rs5632acqd83fl0jb30j2bk2s802mqpd-proof-general-4.5-2.d668946.drv

                          Lint warnings

                          LinterMessageLocation
                          input-labels

                          Identify input labels that do not match package names

                          label 'emacs' does not match package name 'emacs-minimal'
                          input-labels

                          Identify input labels that do not match package names

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