The IT subdirectory is problematic

[andrejbauer]

The IT subdirectory which contains the development of W-types by Steve Awodey and Kristina Sojakova is problematic. It contains a copy Vladimir Voevodsky's Coq files copied over. This is bad because it allows us no way of synchronizing with Vladimir. When Steve copied my Oberwolfach tutorials it didn't matter so much, but now we are reaching a point where we will be sorry for bad practices.

Further, IT/identity/identity.v redefines a lot of stuff that is already defined in paths.v, for example notations such as @, and it makes an incompatible notation p! (whereas in the rest of repository it is !p).

The IT subdirectory is properly a sub-project of Vladimir's files and that's where it should be. It does not even depend on anything else in HoTT.

I think we have reached a stage when we have to be far more conservative about accepting things into the main HoTT repository. The repository is watched by 30 people and forked by 14, and we should care about them.

I propose that IT be removed from HoTT. It can of course still live on Kristina's fork, nobody is forcing her to do anything.

We also need to set clear guidelines about what gets accepted. For example, I think we should never accept a pull request which has insufficient description of changes. The person who accepts a pull request should read every single change made to the repository, etc.

We could also consider reducing the number of people who are permitted to make pull requests. This seems to work well. For example, in my project on the eff programming language, Matija Pretnar is the only person who can accept pull requests, even though I am a co-author of the language. This way a certain level of coherence is achieved.

Let me know what you think.

[mikeshulman]

I agree; thanks for bringing this up.

[andrejbauer]

You agree with what? Let me be more specific:

(a) we remove IT (b) we become a bit stricter about accepting stuff

One issue can be resolved very easily, while the other probably requires a bit of discussion.

[mikeshulman]

I agree that we should do (a) and that it's worth discussing (b). I don't object to the idea of having only one pull-request-accepter, but it might not be necessary if all the pull-request-accepters could agree on consistent standards. I'm interested to hear what others think.

On Mon, Mar 19, 2012 at 00:24, andrejbauer reply@reply.github.com wrote:

You agree with what? Let me be more specific:

(a) we remove IT (b) we become a bit stricter about accepting stuff

One issue can be resolved very easily, while the other probably requires a bit of discussion.

---

Reply to this email directly or view it on GitHub: https://github.com/HoTT/HoTT/issues/10#issuecomment-4568752

[awodey]

this is ok with us. we'll make the necessary changes (at some point), and then try again.

we will have to the long-postponed discussion about permitted notation, and permitted variants, at some point, though. the best thing would be to allow for person preferences through the use of local macros.

Steve

On Mar 18, 2012, at 2:56 PM, andrejbauer wrote:

The IT subdirectory which contains the development of W-types by Steve Awodey and Kristina Sojakova is problematic. It contains a copy Vladimir Voevodsky's Coq files copied over. This is bad because it allows us no way of synchronizing with Vladimir. When Steve copied my Oberwolfach tutorials it didn't matter so much, but now we are reaching a point where we will be sorry for bad practices.

Further, IT/identity/identity.v redefines a lot of stuff that is already defined in paths.v, for example notations such as @, and it makes an incompatible notation p! (whereas in the rest of repository it is !p).

I think we have reached a stage when we have to be far more conservative about accepting things into the main HoTT repository. The repository is watched by 30 people and forked by 14, and we should care about them.

I propose that IT be removed from HoTT. It can of course still live on Kristina's fork, nobody is forcing her to do anything.

We also need to set clear guidelines about what gets accepted. For example, I think we should never accept a pull request which has insufficient description of changes. The person who accepts a pull request should read every single change made to the repository, etc.

We could also consider reducing the number of people who are permitted to make pull requests. This seems to work well. For example, in my project on the eff programming language, Matija Pretnar is the only person who can accept pull requests, even though I am a co-author of the language. This way a certain level of coherence is achieved.

Let me know what you think.

---

Reply to this email directly or view it on GitHub: https://github.com/HoTT/HoTT/issues/10

[spitters]

As an intermediate workaround one could include Vladimir's repo as a git submodule. In this way HoTT will automatically be in sync with his repo.

Bas

On Sun, Mar 18, 2012 at 8:56 PM, andrejbauer reply@reply.github.com wrote:

The IT subdirectory which contains the development of W-types by Steve Awodey and Kristina Sojakova is problematic. It contains a copy Vladimir Voevodsky's Coq files copied over. This is bad because it allows us no way of synchronizing with Vladimir. When Steve copied my Oberwolfach tutorials it didn't matter so much, but now we are reaching a point where we will be sorry for bad practices.

Further, IT/identity/identity.v redefines a lot of stuff that is already defined in paths.v, for example notations such as @, and it makes an incompatible notation p! (whereas in the rest of repository it is !p).

I think we have reached a stage when we have to be far more conservative about accepting things into the main HoTT repository. The repository is watched by 30 people and forked by 14, and we should care about them.

I propose that IT be removed from HoTT. It can of course still live on Kristina's fork, nobody is forcing her to do anything.

We also need to set clear guidelines about what gets accepted. For example, I think we should never accept a pull request which has insufficient description of changes. The person who accepts a pull request should read every single change made to the repository, etc.

We could also consider reducing the number of people who are permitted to make pull requests. This seems to work well. For example, in my project on the eff programming language, Matija Pretnar is the only person who can accept pull requests, even though I am a co-author of the language. This way a certain level of coherence is achieved.

Let me know what you think.

---

Reply to this email directly or view it on GitHub: https://github.com/HoTT/HoTT/issues/10

[andrejbauer]

It makes far more sense for Kristina to fork Vladimir's repository and then add her stuff to it. I see no reason to keep Vladimir's stuff as a submodule of HoTT. What purpose would that serve?

[awodey]

I would think that HoTT needs to be able to use Vladimir's development, rather than doing everything in parallel. Are you against that?

[andrejbauer]

That's a loaded question. I stated before that I see nothing wrong with having several developments running in parallel. It is way too early for us to know which way is "the best" and it would be detrimental to development of hott if we all decided to use a single setup. I would like to see an Agda development, for example. I have forked off HoTT and changed notation fr paths back to ~~>. Eventually I might make a pull request, but if it is not accepted, I won't really care that much.

If there is one thing I am "against", it is "building the foundation". There is no such thing. We are investigating "a" foundation.

Let me be a bit more specific. There are several ways in which we could improve our and Vladimir files: by patching Coq, by writing beter tactics, by using canonical structures, by using type classes, etc. Vladimir has produced an amazing amount of stuff. It is impossible to experiment with his files, because of the sheer number of results that are in there. It will take me two days to perform an experiment with canonical structures in our HoTT repository, but with Vladimir's I dare not think about it. So, our repository is better for experimenting on how to set things up, and Vladimir's is better because it contains many many amazing results.

And actually, I do not know what you mean by "use Vladimir's development". Import it wholesale? Yes, I am "against" that for reasons stated.

[awodey]

o, complicated ...

Vladimir has done a lot of useful stuff that we want to be able to reuse. So first we did it by taking the parts of his repo that we needed and simply copied them over. The you complained that that was the wrong way to do things, we need to fork the repo or use a submodule or something. Now you don't want that, but instead want everything in the HoTT repo to be independent of Vladimir's files? Or what? How does one reuse Vladimir's files within other things being done in the HoTT repo?

[mikeshulman]

I definitely see an attraction to eventually being able to merge at least the "basics", so that it is easier to share new code around and the community doesn't bifurcate according to which codebase we start from. Just like there is an advantage to having a standard C library, and a standard Coq library, I think eventually it would be good to have a standard homotopy-type-theory library (one for Coq and one for Agda, of course, and one for any other proof assistant that may be created in the future). It's open to debate what should be included in the "basics", and I hope that one of the results of next year at the IAS will be some sort of place to start from on this, and a system for considering future inclusions (although undoubtedly not everyone will be satisfied with the result!). I agree that it's useful to have branches with different purposes, but when there is a basic core of things (like the theory of paths, fibrations, equivalences, and univalence) which is going to get used by almost everything, it would be nice to have that shared in common by everyone so that individual projects can be combined more modularly.

But I don't think that copying one repository wholesale into another (even if as a "submodule" so that it gets updated correctly) is the right way to go about it. Merging the two is probably going to require starting with one of them and deciding, bit-by-bit, what parts of the other to include, what to rename to match the other, what to exclude from the "basic" library as peripheral, and so on.

(Off-topic: Andrej, I hope that your notation-change is on a separate branch from your substantive changes, like improvements to the Circle and removal of the old 8.2-compatibility, so that even if others of us don't want ~~> we can benefit from those?)

[mikeshulman]

Steve, does anything in the IT directory pull in stuff from both the HoTT code and from vladimir's code? I didn't think that was possible, since the two even use different definitions of the path-type.

[andrejbauer]

Right now I think you have two options. The first option is to fork off Vladimir and do stuff there. The other option is to fork off HoTT and do stuff there. I used to have Vladimir's stuff as a submodule, but that served no purpose. So that was clearly wrong.

Perhaps we have different ideas about what the HoTT repository is for.

[awodey]

no, just the basic from Vladimir's Foundations.

I agree that we just need a common basis that other projects can use. Probably the sensible time to develop this systematically is next fall at IAS. Meanwhile, we just need to be able work with what we have and read each other's files.

[andrejbauer]

You will notice that I have proposed that the IT subdirectory be deleted, but have not done so. I think a pull request, or a proposal such as mine, has to be accepted by someone other than the person requesting the pull (as long as we have an oligarchy, it would be different with a benevolet dictator). If nobody does it, that's fine by me, I won't mind.

I have already deleted IT in my fork where such a change doesn't bother anyone. That's the beauty of github.

[awodey]

that was a reply to Mike, not to Andrej.

[mikeshulman]

I think a source code repository should be a collection of related code -- related in the technical sense, rather than the semantic sense. Two pieces of software with the same function (e.g. Firefox and Internet Explorer), but which do not actually incorporate each other's code, are nevertheless separate software projects, and should live in different source code repositories.

If we wanted to make a start on unifying things, we could create a new "basic stuff" repository to include as a submodule into both (perhaps a fork of) HoTT and (presumably a fork of) Vladimir's repository, and start gradually moving things into the "basic" repository as we modify both of the other codebases to use the same basic definitions and names.

[mikeshulman]

Steve: Okay, given that the IT code is only using Vladimir's foundations, not anything from the HoTT code, I would say that "reusing Vladimir's files within other things being done in the HoTT repo" is not the right perspective. Not everything done under the general heading of "the homotopy type theory programme" needs to be put into a single source code repository.

[andrejbauer]

Before I started ths issue I checked that IT uses nothing from HoTT. Are we getting close to closing the issue?

[awodey]

so the conclusion is to be that the IT directory cannot be included in HoTT even after we resolve the notational conflicts because it uses some of Vladimir's code? And in general that nothing that uses Vladimir's code can be included in the HoTT repo in any way? This seems like a absurd rule.

[andrejbauer]

But you use only Vladimir's code and none of HoTT. Why would your code be in HoTT?

[awodey]

because it is a basic part of the entire theory, that other developments can build on.

[mikeshulman]

It sounds like Andrej is right that we have different ideas about what the HoTT repository is for. I don't think a single source code repository is the right place to try to collect every piece of code that formalizes part of the theory, if they are unrelated to each other code-wise; that's not what a source code repository is for. Separate developments of the theory using separate codebases should be in separate repositories, regardless of how basic they are. Someone who wants to build on one of them can then fork the appropriate repository without dragging in any baggage from a different development that they won't be using. Since no one (at present) can build on both the HoTT code and vladimir's code, they should be in separate repositories.

A web page, like http://homotopytypetheory.org/coq/, is a better place to keep a record of, and pointers to, all code that has anything to do with the project.

[mikeshulman]

On the other hand, Steve, I notice that you said "even after we resolve the notational conflicts". Can you elaborate on what you are referring to? I'm wondering whether Andrej and I have misunderstood your intent.

[awodey]

as I understood it, there were two issues: (1) notational conflicts like !f vs. f! and (2) using Vladimir's code. (1) is easily remedied and we can certainly do that, but it sounds as though there are objections to (2).
Are you proposing that anything that uses any part of Vladimir's code belongs in a separate repo? That seems absurd to me. Why would we not want to use parts of Vladimir's code (or allow anyone else working here to use it, even if you choose not to)?

Is it then OK to instead rewrite -- essentially copying -- those parts of Vladimir's code that one wants to use, maybe revising the notation a bit to make it look different? What is the point of that?

If it's a matter of compatibility with the rest of the development, as in (1), then I understand; but if it's some sort of conceptual purity, then I don't.

[awodey]

OK, I give up. Please remove the IT subdirectory from the HoTT repo -- we'll have it live somewhere else. Sorry you don't like it -- maybe you'll make your own HoTT inductive types.

Please state some rules that will allow users like me to contribute to HoTT in the future without such negotiations. Thanks.

[mikeshulman]

I'm really sad that we're failing to communicate effectively here! But I still have hope that if we have the patience to continue, eventually we'll understand what each other is saying.

The issue is exactly compatibility with the rest of the development, not any sort of objection to Vladimir's code on principle. However, I don't think compatibility means just visual compatibility in the sense of using similar notation, but being based on the same definitions. For instance, Vladimir's code says

Notation paths := identity .

whereas the HoTT code says

Inductive paths {A} : A -> A -> Type := idpath : forall x, paths x x.

These are incompatible. A given piece of code cannot import both the HoTT codebase and Vladimir's codebase and put together theorems from the two codebases to prove something new about paths, because the word paths means something different to the HoTT theorems than it does to Vladimir's theorems. Similarly, Vladimir's code says

Record total2 { T: Type } ( P: T -> Type ) := tpair { pr1 : T ; pr2 : P pr1 }. 

whereas the HoTT code uses Coq's built-in sigT. Vladimir defines

Definition idfun ( T : UU ) := fun t : T => t .

whereas HoTT defines

Definition idmap A := fun x : A => x.

And so on. I don't like this state of affairs in the long run, but as long as it is the case, nothing that builds on Vladimir's unmodified code is compatible with the HoTT code, and vice versa, regardless of whether they use similar notation or not. There is nothing wrong with using Vladimir's code! But it should be in a separate repository. It's not a question of "allowing" people to use Vladimir's code; no one is making a rule that everyone working on homotopy type theory can only work with branches of this repository. Anyone who wants to build a development on Vladimir's codebase should fork his repository and do their work there.

On the other hand, if one were to take (some part of) Vladimir's code and modify it so that it uses the underlying definitions etc. from the HoTT code (literally, i.e. by importing them), then that piece of code would become compatible with the HoTT code (and incompatible with Vladimir's unmodified code). That modified code, and anything else built on it, I think it would make perfect sense to include in the HoTT repository.

[mikeshulman]

Perhaps it was a mistake for us to name this repository "HoTT". I can see how that may give the impression that this is the repository for all code that has anything to do with homotopy type theory.

[andrejbauer]

Yes, there is a basic misunderstanding that would be trivially resolved in person.

[spitters]

Allow me to add a bit to the misunderstanding.

1. "HoTT" and "univalent" seem to be building the same "HoTT" foundation, but the implementation is different.
2. Perhaps we can persuade Vladimir to use the HoTT repository, if one could port his code to HoTT. The univalent library is not that big and quite similar to HoTT: 771 848 228 Generalities/uu0.v 17 0 17 Generalities/uuu.v 44 21 32 hlevel1/hProp.v 573 275 144 hlevel2/algebra1.v 90 6 34 hlevel2/finitesets.v 171 126 52 hlevel2/hnat.v 155 100 58 hlevel2/hSet.v 35 15 17 hlevel2/hz.v 61 72 27 hlevel2/stnfsets.v 22 24 15 Proof_of_Extensionality/funextfun.v 1939 1487 624 total

Best,

Bas

[andrejbauer]

Bas, any estimate how much work this would be? And someone should talk to Vladimir before we embark on such a thing.

[spitters]

Perhaps, a month is a conservative estimate. Once the basic definitions have been replaced, most of the proofs should go through. The best way to find out would be to try to replace the definitions in the way Mike suggests and see whether one can get the files in Generalities to compile. Once this is done, one can start to do further cleanups by comparing with the lemmas in the HoTT directory.

Best,

Bas

On Wed, Apr 4, 2012 at 10:45 AM, andrejbauer reply@reply.github.com wrote:

Bas, any estimate how much work this would be? And someone should talk to Vladimir before we embark on such a thing.

---

Reply to this email directly or view it on GitHub: https://github.com/HoTT/HoTT/issues/10#issuecomment-4949493