asr / apia

Haskell program for proving first-order theorems written in Agda using automatic theorem provers for first-order logic
MIT License
6 stars 0 forks source link

Failed Apia in 8.0.2 #93

Closed jonaprieto closed 7 years ago

jonaprieto commented 7 years ago

@asr I was not sure it was a problem of Apia or my computer and its ghc version, but today, I got the same error message in Fedora 24,

$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 8.0.2
$ cabal --version
cabal-install version 1.24.0.2
compiled using version 1.24.2.0 of the Cabal library 
$ agda --version
Agda version 2.6.0.1-5893007
$ make install-bin
cabal install --disable-documentation
Warning: cannot determine version of /usr/local/bin/hpc :
""
Resolving dependencies...
Configuring apia-1.0.1...
Building apia-1.0.1...
Failed to install apia-1.0.1
Build log ( /home/hotel/.cabal/logs/apia-1.0.1.log ):
cabal: Entering directory '.'
Configuring apia-1.0.1...
Building apia-1.0.1...
Preprocessing executable 'apia' for apia-1.0.1...
[38 of 40] Compiling Apia.Translation.Functions ( src/Apia/Translation/Functions.hs, dist/build/apia/apia-tmp/Apia/Translation/Functions.o )

src/Apia/Translation/Functions.hs:119:30: error:
    • The constructor ‘Clause’ should have 6 arguments, but has been given 7
    • In the pattern: Clause lr fr tel (_ : ncps) (Just cBody) cTy cc
      In an equation for ‘clauseToFormula’:
          clauseToFormula
            qName
            ty
            cl@(Clause lr fr tel (_ : ncps) (Just cBody) cTy cc)
            totalBoundedVars
            = do { reportSLn "def2f" 20 $ "cl: " ++ show cl;
                   case tel of {
                     ExtendTel (Dom _ (El (Type (Max [])) (Def _ []))) (Abs x tels)
                       -> ...
                     ExtendTel (Dom _ (El (Type (Max [])) (Def _ _))) (Abs _ _)
                       -> tErr $ ProofTermInDefintion qName
                     ExtendTel (Dom _ (El (Type (Max [])) (Pi _ _))) _
                       -> tErr $ NoFOLDefinition qName
                     ExtendTel (Dom _ (El (Type (Max [_])) (Sort _))) _
                       -> tErr $ NoFOLDefinition qName
                     _ -> ... } }
cabal: Leaving directory '.'
cabal: Error: some packages failed to install:
apia-1.0.1 failed during the building phase. The exception was:
ExitFailure 1
Makefile:490: recipe for target 'install-bin' failed
make: *** [install-bin] Error 1
$ 

No idea.

asr commented 7 years ago

You need to update eagda.