Agda-stdlib: Release version compatible with Agda 2.5.3

[asr]

Note that a release procedure is described here. @MatthewDaggitt, please ask if you need some help.

[MatthewDaggitt]

Thanks, will try on Monday.

[MatthewDaggitt]

Okay I'm on the following step (having completed all previous steps)

• Update submodule commit for the stable library in Agda:
  cd agda
  make fast-forward-std-lib
  record-the-changes-and-push

But when I run make fast-forward-std-lib I get the following output:

git submodule update --init --remote std-lib
make[1]: Entering directory '/auto/homes/mld46/Code/agda-update/std-lib'
cabal clean && cabal install
cleaning...
Resolving dependencies...
Configuring lib-0.13...
Building lib-0.13...
Preprocessing executable 'GenerateEverything' for lib-0.13...
[1 of 1] Compiling Main             ( GenerateEverything.hs, dist/build/GenerateEverything/GenerateEverything-tmp/Main.o )
Linking dist/build/GenerateEverything/GenerateEverything ...
Preprocessing executable 'AllNonAsciiChars' for lib-0.13...
[1 of 1] Compiling Main             ( AllNonAsciiChars.hs, dist/build/AllNonAsciiChars/AllNonAsciiChars-tmp/Main.o )
Linking dist/build/AllNonAsciiChars/AllNonAsciiChars ...
Installing executable(s) in /home/mld46/.cabal/bin
Installed lib-0.13
cabal exec -- GenerateEverything
make[1]: Leaving directory '/auto/homes/mld46/Code/agda-update/std-lib'

which implies its not finding the new 0.14 version/tag that's up on github.

[asr]

The above command works for me:

$ make fast-forward-std-lib 
git submodule update --init --remote std-lib
Submodule path 'std-lib': checked out 'db160802e15b4661ae86486e7feb68934614b7f0'
make[1]: Entering directory '<PATH>/std-lib'
cabal clean && cabal install
cleaning...
Resolving dependencies...
Configuring lib-0.14...
Preprocessing executable 'GenerateEverything' for lib-0.14..
Building executable 'GenerateEverything' for lib-0.14..
[1 of 1] Compiling Main             ( GenerateEverything.hs, dist/build/GenerateEverything/GenerateEverything-tmp/Main.o )
Linking dist/build/GenerateEverything/GenerateEverything ...
Preprocessing executable 'AllNonAsciiChars' for lib-0.14..
Building executable 'AllNonAsciiChars' for lib-0.14..
[1 of 1] Compiling Main             ( AllNonAsciiChars.hs, dist/build/AllNonAsciiChars/AllNonAsciiChars-tmp/Main.o )
Linking dist/build/AllNonAsciiChars/AllNonAsciiChars ...
Installing executable GenerateEverything in /home/asr/.cabal/bin
Installing executable AllNonAsciiChars in /home/asr/.cabal/bin
Installed lib-0.14
cabal exec -- GenerateEverything
make[1]: Leaving directory '<PATH>/std-lib'

I'm using

$ git --version
git version 2.14.1

what about you?

[MatthewDaggitt]

I get git version 2.7.4, but when I try and update git I get git is already the newest version (1:2.7.4-0ubuntu1.2).

I think my version of git is fine. It's just that it's not detecting the latest version of the submodule... Do I need to change something in the makefile to make it target the new tag v0.14?

[MatthewDaggitt]

Hmm okay fixed by deleting and re-cloning the repository.

Next question. What does the instruction record-the-changes-and-push mean? It doesn't seem to be a git command or a target in the make-file.

Does it just mean commit the changes?

[asr]

Does it just mean commit the changes?

Yes. Sorry for the confusion.

[MatthewDaggitt]

Okay. Then it's all done except announcing it to the mailing list.

This should be the easiest part, but how do I do this? :) I don't seem to have access to either list.

[andreasabel]

Does this mean you currently cannot enroll to the Agda-list at

https://lists.chalmers.se/mailman/listinfo/agda

?
See https://github.com/agda/agda/issues/2736#issuecomment-328512389
I emailed our IT-support about it.

[MatthewDaggitt]

Yes I get a 403 Forbidden error when I try that link.

[MatthewDaggitt]

I guess the best solution until its resolved, is for someone else with access to send an email out to the list.

[asr]

Unfortunately in which Agda branch (master or stable-2.5) to "merge" which standard library branch hasn't a stable procedure. Anyway, I cherry-picked your commit in the Agda master branch into the Agda stable-2.5 branch because the master branch of the standard library is compatible which that Agda branch.

[andreasabel]

Yes I get a 403 Forbidden error when I try that link.
Please email me your IP and browser version.

[MatthewDaggitt]

@asr Apologies. To clarify I should have updated the standard library version in the stable-2.5 branch?

[asr]

I guess the best solution until its resolved, is for someone else with access to send an email out to the list.

@MatthewDaggitt, I disagree. You should to make the announce.

[asr]

@asr Apologies. To clarify I should have updated the standard library version in the stable-2.5 branch?

Yes and to merge your commit in the stable-2.5 branch into the master branch.

[MatthewDaggitt]

@asr okay, I will remember that for next time. Thank you for all your help!

[asr]

Please keep in mind that next time it would be different if the different branches of Agda require different branches of the standard library.

[MatthewDaggitt]

Okay.

[gallais]

I guess this can be closed? I see that 0.14 is on the wiki.

[MatthewDaggitt]

So the only thing remaining is to announce it on the mailing list. @asr is very kind in saying that I should do it but I still don't have permission to access it (see the comments at the end of agda/agda#2736). I'm happy to close this otherwise....

[asr]

@andreasabel any news about the 403 error gives by https://lists.chalmers.se/mailman/listinfo/agda?

[andreasabel]

I have pinged my IT-support again about this, their response is overdue.

[UlfNorell]

@MatthewDaggitt: I can subscribe you to the list if you want. Just let me know which address to use. Alternatively you can post a message without being subscribed and I'll approve it manually.

[MatthewDaggitt]

@UlfNorell That'd be great, thanks. Can you use "[email protected]"?
What's the address of the list that I need to send it to?

[UlfNorell]

You should get a welcome mail with the details (let me know if that doesn't happen).

[andreasabel]

IT-support has opened the Agda mailing list page again. (Thanks to an email by our big boss, Peter Dybjer.)

[MatthewDaggitt]

Thanks, have sent out the announcement.