search

RedPRL / sml-telescopes

an abstract data type for telescopes
1 stars 1 forks source link

o Added folding functions. #2

Closed vrahli closed 8 years ago

jonsterling commented 8 years ago

great, thanks!

jonsterling commented 8 years ago

Now that it's merged, if you need to upgrade JonPRL to this version, then check out master from within the telescopes submodule in JonPRL, and then you can commit the updated ref to your branch.

vrahli commented 8 years ago

What should I do to commit the updated ref to my branch?

On Fri, Nov 20, 2015 at 5:13 PM, Jonathan Sterling <notifications@github.com

wrote:

Now that it's merged, if you need to upgrade JonPRL to this version, then check out master from within the telescopes submodule in JonPRL, and then you can commit the updated ref to your branch.

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158446780 .

http://www.cs.cornell.edu/~rahli/

jonsterling commented 8 years ago

So, imagine that you're in the root of the JonPRL project. Here's some instructions (from memory, so they may not be exactly right)

cd lib/sml-telescopes
git checkout master
git pull origin master
cd ../.. # i.e. go back to the root of the JonPRL project
git status
# now you will see that the sml-telescopes submodule pointer has changed
git add . # stage the changed pointer
git commit -m "Updated sml-telescopes submodule"
vrahli commented 8 years ago

I'd done everything up to the git status, but then something tells me that the sml-telescopes module pointer has changed.

$ git status On branch export2coq Your branch is up-to-date with 'origin/export2coq'. nothing to commit, working directory clean

Should I still run git add . and git commit -m "..."?

On Fri, Nov 20, 2015 at 5:18 PM, Jonathan Sterling <notifications@github.com

wrote:

So, imagine that you're in the root of the JonPRL project. Here's some instructions (from memory, so they may not be exactly right)

cd lib/sml-telescopes git checkout master git pull origin mastercd ../.. # i.e. go back to the root of the JonPRL project git status# now you will see that the sml-telescopes submodule pointer has changed git add . # stage the changed pointer git commit -m "Updated sml-telescopes submodule"

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158448019 .

http://www.cs.cornell.edu/~rahli/

jonsterling commented 8 years ago

Can you paste the output that you're seeing?

vrahli commented 8 years ago

The ouyput at the root of JonPRL is:

$ git status On branch export2coq Your branch is up-to-date with 'origin/export2coq'. nothing to commit, working directory clean

However, the output at the root of sml-telescopes is:

$ git status HEAD detached at 63066aa nothing to commit, working directory clean

This is actually what I get now that I've pull from origin master (in sml-telescopes). Before pulling I got:

$ git status On branch master Your branch is behind 'origin/master' by 1 commit, and can be fast-forwarded. (use "git pull" to update your local branch) nothing to commit, working directory clean

On Fri, Nov 20, 2015 at 5:27 PM, Jonathan Sterling <notifications@github.com

wrote:

Can you paste the output that you're seeing?

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158450933 .

http://www.cs.cornell.edu/~rahli/

jonsterling commented 8 years ago

OK, that's kind of weird.

Inside sml-telescopes, can you run "git fetch origin; git reset --hard origin/master"? Then, run "git status" in sml-telescopes.

On Fri, Nov 20, 2015, at 08:31 AM, Vincent Rahli wrote:

The ouyput at the root of JonPRL is:

$ git status On branch export2coq Your branch is up-to-date with 'origin/export2coq'. nothing to commit, working directory clean

However, the output at the root of sml-telescopes is:

$ git status HEAD detached at 63066aa nothing to commit, working directory clean

This is actually what I get now that I've pull from origin master (in sml-telescopes). Before pulling I got:

$ git status On branch master Your branch is behind 'origin/master' by 1 commit, and can be fast-forwarded. (use "git pull" to update your local branch) nothing to commit, working directory clean

On Fri, Nov 20, 2015 at 5:27 PM, Jonathan Sterling <notifications@github.com

wrote:

Can you paste the output that you're seeing?

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158450933 .

http://www.cs.cornell.edu/~rahli/

Reply to this email directly or view it on GitHub: https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158451859

jonsterling commented 8 years ago

Hmm, for some reason GitHub is mangling our responses. Might be better to switch to emial.

vrahli commented 8 years ago

I had to run another git checkout maser for some reason and now I get (in sml-telescopes):

$ git status On branch master Your branch is up-to-date with 'origin/master'. nothing to commit, working directory clean

And now at JonPRL root I get:

$ git status On branch export2coq Your branch is up-to-date with 'origin/export2coq'. Changes not staged for commit: (use "git add ..." to update what will be committed) (use "git checkout -- ..." to discard changes in working directory)

modified:   lib/sml-telescopes (new commits)

no changes added to commit (use "git add" and/or "git commit -a")

What next?

On Fri, Nov 20, 2015 at 5:38 PM, Jonathan Sterling <notifications@github.com

wrote:

OK, that's kind of weird.

Inside sml-telescopes, can you run "git fetch origin; git reset --hard origin/master"? Then, run "git status" in sml-telescopes.

On Fri, Nov 20, 2015, at 08:31 AM, Vincent Rahli wrote:

The ouyput at the root of JonPRL is:

$ git status On branch export2coq Your branch is up-to-date with 'origin/export2coq'. nothing to commit, working directory clean

However, the output at the root of sml-telescopes is:

$ git status HEAD detached at 63066aa nothing to commit, working directory clean

This is actually what I get now that I've pull from origin master (in sml-telescopes). Before pulling I got:

$ git status On branch master Your branch is behind 'origin/master' by 1 commit, and can be fast-forwarded. (use "git pull" to update your local branch) nothing to commit, working directory clean

On Fri, Nov 20, 2015 at 5:27 PM, Jonathan Sterling <notifications@github.com

wrote:

Can you paste the output that you're seeing?

— Reply to this email directly or view it on GitHub < https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158450933

.

http://www.cs.cornell.edu/~rahli/

Reply to this email directly or view it on GitHub:

https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158451859

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158453597 .

http://www.cs.cornell.edu/~rahli/

jonsterling commented 8 years ago

OK; now, can you run "git add lib/sml-telescopes"? Then, you should be able to commit the changes to JonPRL.

Best, Jon

On Fri, Nov 20, 2015, at 08:50 AM, Vincent Rahli wrote:

I had to run another git checkout maser for some reason and now I get (in sml-telescopes):

$ git status On branch master Your branch is up-to-date with 'origin/master'. nothing to commit, working directory clean

And now at JonPRL root I get:

$ git status On branch export2coq Your branch is up-to-date with 'origin/export2coq'. Changes not staged for commit: (use "git add ..." to update what will be committed) (use "git checkout -- ..." to discard changes in working directory)

modified:   lib/sml-telescopes (new commits)

no changes added to commit (use "git add" and/or "git commit -a")

What next?

On Fri, Nov 20, 2015 at 5:38 PM, Jonathan Sterling <notifications@github.com

wrote:

OK, that's kind of weird.

Inside sml-telescopes, can you run "git fetch origin; git reset --hard origin/master"? Then, run "git status" in sml-telescopes.

On Fri, Nov 20, 2015, at 08:31 AM, Vincent Rahli wrote:

The ouyput at the root of JonPRL is:

$ git status On branch export2coq Your branch is up-to-date with 'origin/export2coq'. nothing to commit, working directory clean

However, the output at the root of sml-telescopes is:

$ git status HEAD detached at 63066aa nothing to commit, working directory clean

This is actually what I get now that I've pull from origin master (in sml-telescopes). Before pulling I got:

$ git status On branch master Your branch is behind 'origin/master' by 1 commit, and can be fast-forwarded. (use "git pull" to update your local branch) nothing to commit, working directory clean

On Fri, Nov 20, 2015 at 5:27 PM, Jonathan Sterling <notifications@github.com

wrote:

Can you paste the output that you're seeing?

— Reply to this email directly or view it on GitHub < https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158450933

.

http://www.cs.cornell.edu/~rahli/

Reply to this email directly or view it on GitHub:

https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158451859

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158453597 .

http://www.cs.cornell.edu/~rahli/

Reply to this email directly or view it on GitHub: https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158457266

jonsterling commented 8 years ago

Ah, I see from the commit log that you have got it working :)

-- jon

On Fri, Nov 20, 2015, at 09:11 AM, Jon Sterling wrote:

OK; now, can you run "git add lib/sml-telescopes"? Then, you should be able to commit the changes to JonPRL.

Best, Jon

On Fri, Nov 20, 2015, at 08:50 AM, Vincent Rahli wrote:

I had to run another git checkout maser for some reason and now I get (in sml-telescopes):

$ git status On branch master Your branch is up-to-date with 'origin/master'. nothing to commit, working directory clean

And now at JonPRL root I get:

$ git status On branch export2coq Your branch is up-to-date with 'origin/export2coq'. Changes not staged for commit: (use "git add ..." to update what will be committed) (use "git checkout -- ..." to discard changes in working directory)

modified:   lib/sml-telescopes (new commits)

no changes added to commit (use "git add" and/or "git commit -a")

What next?

On Fri, Nov 20, 2015 at 5:38 PM, Jonathan Sterling <notifications@github.com

wrote:

OK, that's kind of weird.

Inside sml-telescopes, can you run "git fetch origin; git reset --hard origin/master"? Then, run "git status" in sml-telescopes.

On Fri, Nov 20, 2015, at 08:31 AM, Vincent Rahli wrote:

The ouyput at the root of JonPRL is:

$ git status On branch export2coq Your branch is up-to-date with 'origin/export2coq'. nothing to commit, working directory clean

However, the output at the root of sml-telescopes is:

$ git status HEAD detached at 63066aa nothing to commit, working directory clean

This is actually what I get now that I've pull from origin master (in sml-telescopes). Before pulling I got:

$ git status On branch master Your branch is behind 'origin/master' by 1 commit, and can be fast-forwarded. (use "git pull" to update your local branch) nothing to commit, working directory clean

On Fri, Nov 20, 2015 at 5:27 PM, Jonathan Sterling <notifications@github.com

wrote:

Can you paste the output that you're seeing?

— Reply to this email directly or view it on GitHub < https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158450933

.

http://www.cs.cornell.edu/~rahli/

Reply to this email directly or view it on GitHub:

https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158451859

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158453597 .

http://www.cs.cornell.edu/~rahli/

Reply to this email directly or view it on GitHub: https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158457266

vrahli commented 8 years ago

Actually I get this error on both machines. Which makes sense? Should I just add back the signature of fresh in TELESCOPES?

On Fri, Nov 20, 2015 at 11:47 PM, vincent rahli vincent.rahli@gmail.com wrote:

On my machine at home I'm getting the following error: src/refiner/context.fun:16.15-16.30 Error: unbound variable or constructor: fresh in path Telescope.fresh For some reason I wasn't getting the error on my machine at work I think. But it's true that fresh is gone from the signature of telescopes and is used in context. Any idea what I should do?

On Fri, Nov 20, 2015 at 6:17 PM, Jonathan Sterling < notifications@github.com> wrote:

Ah, I see from the commit log that you have got it working :)

-- jon

On Fri, Nov 20, 2015, at 09:11 AM, Jon Sterling wrote:

OK; now, can you run "git add lib/sml-telescopes"? Then, you should be able to commit the changes to JonPRL.

Best, Jon

On Fri, Nov 20, 2015, at 08:50 AM, Vincent Rahli wrote:

I had to run another git checkout maser for some reason and now I get (in sml-telescopes):

$ git status On branch master Your branch is up-to-date with 'origin/master'. nothing to commit, working directory clean

And now at JonPRL root I get:

$ git status On branch export2coq Your branch is up-to-date with 'origin/export2coq'. Changes not staged for commit: (use "git add ..." to update what will be committed) (use "git checkout -- ..." to discard changes in working directory)

modified: lib/sml-telescopes (new commits)

no changes added to commit (use "git add" and/or "git commit -a")

What next?

On Fri, Nov 20, 2015 at 5:38 PM, Jonathan Sterling <notifications@github.com

wrote:

OK, that's kind of weird.

Inside sml-telescopes, can you run "git fetch origin; git reset --hard origin/master"? Then, run "git status" in sml-telescopes.

On Fri, Nov 20, 2015, at 08:31 AM, Vincent Rahli wrote:

The ouyput at the root of JonPRL is:

$ git status On branch export2coq Your branch is up-to-date with 'origin/export2coq'. nothing to commit, working directory clean

However, the output at the root of sml-telescopes is:

$ git status HEAD detached at 63066aa nothing to commit, working directory clean

This is actually what I get now that I've pull from origin master (in sml-telescopes). Before pulling I got:

$ git status On branch master Your branch is behind 'origin/master' by 1 commit, and can be fast-forwarded. (use "git pull" to update your local branch) nothing to commit, working directory clean

On Fri, Nov 20, 2015 at 5:27 PM, Jonathan Sterling <notifications@github.com

wrote:

Can you paste the output that you're seeing?

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

https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158450933

.

http://www.cs.cornell.edu/~rahli/

Reply to this email directly or view it on GitHub:

https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158451859

— Reply to this email directly or view it on GitHub < https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158453597

.

http://www.cs.cornell.edu/~rahli/

Reply to this email directly or view it on GitHub:

https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158457266

— Reply to this email directly or view it on GitHub https://github.com/jonsterling/sml-telescopes/pull/2#issuecomment-158463987 .

http://www.cs.cornell.edu/~rahli/

http://www.cs.cornell.edu/~rahli/

jonsterling commented 8 years ago

@vrahli I think what happened is that I removed fresh from the telescopes lib since I didn't want it in there, but I didn't update JonPRL yet... Feel free to just add it back to the signature here if that gets things working again for you.