search

jonsterling / TT-Reflection

An experimental type theory with scoped equality reflection, and non-arbitrary proof search. This is basically a pared down version of Andromeda/Brazil, but with untyped reduction and a more Nuprl-like feel. Computational content of proofs is got via a realizability-based extraction. (Note: substitution is unsafe here, not because of a problem with the theory, but because I didn't understand how Bound works sadly.)
12 stars 0 forks source link

Add a simple command-line user interface #15

Closed ghost closed 10 years ago

jonsterling commented 10 years ago

Whoa, cool! I'm glad to see someone other than myself has figured out how to use the new Vinyl :)

ghost commented 10 years ago

Yeah, had to figure out some of the new stuff but it was pretty painless :)

Not sure if you want to depend on vinyl and some of the other stuff though. Let me know if you'd prefer to do something differently.

jonsterling commented 10 years ago

Seems pretty harmless! I'll review it in more detail tomorrow once I'm at my office though. Evan/computionist had patched this to be compatible with GHC 7.6, so I might want to get the 7.6 compat PR merged into Vinyl that I have been dragging my feet on.

ghost commented 10 years ago

Sounds good :)

It wouldn't be too hard to switch back to plain records if that becomes a bigger task than expected. I'm happy to test or help with something on the 7.6/Vinyl side too.

jonsterling commented 10 years ago
ghost commented 10 years ago

Cool, I'll make the changes you suggested and push an update probably later today.

ghost commented 10 years ago

Made the changes you suggested. Note the updated cabal constraints. Let me know if that causes breakage somehow. I did a cabal update and re-built in a fresh sandbox with 7.8.2 just to be sure though.

ghost commented 10 years ago

Hmm, I think the CI build might be failing due to an issue with cabal-install that was fixed after 1.18.0.2. I'm using cabal-install-1.20.0.2, Cabal-1.20.0.1, and ghc-7.8.2.

jonsterling commented 10 years ago

Oh dear...

ghost commented 10 years ago

This is the package database from my sandbox. I think what's happening is that transformers-compat is being used since transformers isn't even installed.

~/TT-Reflection/.cabal-sandbox/x86_64-osx-ghc-7.8.2-packages.conf.d
   QuickCheck-2.7.5
   aeson-0.7.0.6
   ansi-terminal-0.6.1.1
   ansi-wl-pprint-0.6.7.1
   attoparsec-0.12.1.0
   bifunctors-4.1.1.1
   blaze-builder-0.3.3.2
   blaze-html-0.7.0.2
   blaze-markup-0.6.1.0
   bound-1.0.3
   bytes-0.14.0.2
   cereal-0.4.0.1
   charset-0.3.7
   comonad-4.2
   contravariant-0.6
   data-default-class-0.0.1
   digits-0.2
   distributive-0.4.4
   dlist-0.7.0.1
   exceptions-0.6.1
   fingertree-0.1.0.0
   free-4.9
   generic-deriving-1.6.3
   hashable-1.2.2.0
   hashable-extras-0.2.0.1
   haskeline-0.7.1.3
   keys-3.10.1
   lens-4.2
   mtl-2.1.3.1
   nats-0.2
   optparse-applicative-0.9.0
   parallel-3.2.0.4
   parsec-3.1.5
   parsers-0.10.3
   pointed-4.1
   prelude-extras-0.4
   primitive-0.5.3.0
   profunctors-4.0.4
   random-1.0.1.1
   reducers-3.10.2.1
   reflection-1.4
   scientific-0.3.2.1
   semigroupoids-4.0.2.1
   semigroups-0.15
   singletons-1.0
   split-0.2.2
   stm-2.4.3
   syb-0.4.2
   tagged-0.7.2
   terminfo-0.4.0.0
   text-1.1.1.3
   tf-random-0.5
   th-desugar-1.4.0
   transformers-compat-0.3.3.3
   trifecta-1.4.2
   unordered-containers-0.2.4.0
   utf8-string-0.3.8
   vector-0.10.11.0
   vinyl-0.4.2
   void-0.6.1
   zlib-0.5.4.1
ghost commented 10 years ago

I just completely wiped out ~/.cabal and ~/.ghc so I only had the packages installed with ghc-7.8.2. Then I did the following:

cabal sandbox init
cabal update
cabal install --only-dependencies

It's building successfully. Can you try updating cabal-install on the CI instance? This is the issue I was referring to earlier:

http://www.reddit.com/r/haskell/comments/26045a/if_youre_finding_cabal_cant_build_your_project

jonsterling commented 10 years ago

OK, I'll see what can be done once I get to my office. It doesn't actually look like I can upgrade cabal on the CI though—I'll try fiddling with it though.

On Jun 19, 2014, at 8:52 PM, Darin Morrison notifications@github.com wrote:

I just completely wiped out ~/.cabal and ~/.ghc so I only had the packages installed with ghc-7.8.2. Then I did the following:

cabal sandbox init cabal update cabal install --only-dependencies It's building successfully. Can you try updating cabal-install on the CI instance? This is the issue I was referring to earlier:

http://www.reddit.com/r/haskell/comments/26045a/if_youre_finding_cabal_cant_build_your_project

— Reply to this email directly or view it on GitHub.

ghost commented 10 years ago

I think you might be able to upgrade cabal-install during the before_install phase. See item 4: http://docs.travis-ci.com/user/build-configuration/

Perhaps something like the following script might work:

apt-key adv --keyserver keyserver.ubuntu.com --recv-keys F6F88286
echo 'deb     http://ppa.launchpad.net/hvr/ghc/ubuntu precise main' >> /etc/apt/sources.list.d/haskell.list
echo 'deb-src http://ppa.launchpad.net/hvr/ghc/ubuntu precise main' >> /etc/apt/sources.list.d/haskell.list
apt-get update
apt-get install -y --no-install-recommends alex-3.1.3 cabal-install-1.20 ghc-7.8.2 happy-1.19.3    #alex, ghc, happy optional
echo 'PATH=/opt/alex/3.1.3/bin:/opt/cabal/1.20/bin:/opt/ghc/7.8.2/bin:/opt/happy/1.19.3/bin:${PATH}' > /etc/profile.d/haskell.sh   #this may not work if a new login shell isn't created; in that case just update the path manually
jonsterling commented 10 years ago

Hm, even this doesn't build on my machine with a fresh env. I'm going to try and get it working locally, and then I think I've another way to get the newest cabal on travis.

ghost commented 10 years ago

Hmm. Are you using cabal-install-1.20.0.2?

It might work by manually installing transformers-compat or following one of the other alternatives mentioned in that thread.

If that still doesn't work I can try to downgrade my local cabal-install and see if I can get things building with an older version. I sort of hate having to do that though since --allow-newer from 1.20.0.* is so useful.

jonsterling commented 10 years ago

Hm, I was using cabal-install-1.20.0.1. So I did get it to build by changing the fixed versions as follows:

transformers ==0.4.1.0             to              transformers ==0.3.0.0
transformers-compat ==0.3.0.0      to              transformers ==0.3.3.3

But I'll try upgrading my cabal-install and see what happens.

ghost commented 10 years ago

Interesting. What happens if you remove cabal.config and try in a fresh environment locally?

I'll see if I can reproduce a successful build with your change.

jonsterling commented 10 years ago

With cabal-install-1.20.0.1, this is what I get:

Resolving dependencies...
cabal: Could not resolve dependencies:
trying: TT-0.1.0.0 (user goal)
trying: lens-4.2 (dependency of TT-0.1.0.0)
next goal: transformers (dependency of lens-4.2)
rejecting: transformers-0.3.0.0/installed-7df... (global constraint requires
==0.4.1.0)
trying: transformers-0.4.1.0
next goal: trifecta (dependency of TT-0.1.0.0)
rejecting: trifecta-1.4.2 (conflict: transformers==0.4.1.0, trifecta =>
transformers>=0.2 && <0.4)
rejecting: trifecta-1.4.1, 1.4, 1.2.1.1, 1.2.1, 1.2, 1.1, 1.0, 0.53, 0.52,
0.51.0.1, 0.51, 0.50.2.1, 0.50.1, 0.50, 0.49.1, 0.49, 0.47, 0.46, 0.45, 0.44,
0.43, 0.42, 0.41, 0.40, 0.39, 0.38, 0.37, 0.36.3, 0.36.2, 0.36.1, 0.36, 0.35,
0.34, 0.32.1, 0.32, 0.31, 0.30, 0.29, 0.28, 0.27, 0.26, 0.25, 0.24, 0.23,
0.22, 0.21, 0.20, 0.19, 0.18, 0.17, 0.16.1, 0.16, 0.15.1, 0.15, 0.14, 0.13,
0.12, 0.11, 0.10, 0.9, 0.8.0.1, 0.8, 0.7.2, 0.7.1, 0.7, 0.6, 0.5.1, 0.5, 0.4,
0.3, 0.2, 0.1 (global constraint requires ==1.4.2)
Dependency tree exhaustively searched.

Note: when using a sandbox, all packages are required to have consistent
dependencies. Try reinstalling/unregistering the offending packages or
recreating the sandbox.

And here is ghc-pkg list:

/Users/jon/dev/ghc/lib/ghc-7.8.2/package.conf.d
   Cabal-1.18.1.3
   array-0.5.0.0
   base-4.7.0.0
   bin-package-db-0.0.0.0
   binary-0.7.1.0
   bytestring-0.10.4.0
   containers-0.5.5.1
   deepseq-1.3.0.2
   directory-1.2.1.0
   filepath-1.3.0.2
   ghc-7.8.2
   ghc-prim-0.3.1.0
   haskell2010-1.1.2.0
   haskell98-2.0.0.3
   hoopl-3.10.0.1
   hpc-0.6.0.1
   integer-gmp-0.5.1.0
   old-locale-1.0.0.6
   old-time-1.1.0.2
   pretty-1.1.1.1
   process-1.2.0.0
   rts-1.0
   template-haskell-2.9.0.0
   time-1.4.2
   transformers-0.3.0.0
   unix-2.7.0.1

When I remove cabal.config, it works fine, but it uses the different versions of transformers and transformers-compat that I mentioned a few comments ago.

jonsterling commented 10 years ago

Oh weird, I don't know how this would have ever built for you, since your cabal.config had transformers at 0.4x, but trifecta isn't compatible with that at all!

Check http://hackage.haskell.org/package/trifecta

jonsterling commented 10 years ago

Oh thank god, the build passed.

ghost commented 10 years ago

Finally :)