Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Arend language #4777

Closed
wants to merge 3 commits into from
Closed

Add Arend language #4777

wants to merge 3 commits into from

Conversation

ice1000
Copy link

@ice1000 ice1000 commented Jan 19, 2020

Description

Checklist:

@ice1000
Copy link
Author

@ice1000 ice1000 commented Jan 19, 2020

Also, running script/bootstrap also requires libssl-dev on ubuntu, which is not installed by default. It took me about half an hour to figure this out, since the error I saw is "cannot find target to make", instead of "cannot find OpenSSL".

@ice1000
Copy link
Author

@ice1000 ice1000 commented Jan 19, 2020

The license is the MIT license

@ice1000
Copy link
Author

@ice1000 ice1000 commented Jan 19, 2020

Yay! I made the CI passes!

Copy link
Collaborator

@pchaigno pchaigno left a comment

Thanks for the submission!

I'm afraid usage is too low considering our requirements. I counted 20 repositories by 12 users using the extension:ard import OR func search query. Are you expecting usage to grow significantly in the next few months?

@ice1000
Copy link
Author

@ice1000 ice1000 commented Jan 19, 2020

I hope so, let's see.

@ice1000
Copy link
Author

@ice1000 ice1000 commented Feb 13, 2020

There are 300+ (328) files in the search result now :)

@stale
Copy link

@stale stale bot commented Mar 14, 2020

This pull request has been automatically marked as stale because it has not had recent activity, and will be closed if no further activity occurs. If this pull request was overlooked, forgotten, or should remain open for any other reason, please reply here to call attention to it and remove the stale status. Thank you for your contributions.

@stale stale bot added the Stale label Mar 14, 2020
@ice1000
Copy link
Author

@ice1000 ice1000 commented Mar 14, 2020

There's now 340 😟 not much.

@stale stale bot removed the Stale label Mar 14, 2020
@ice1000
Copy link
Author

@ice1000 ice1000 commented Mar 24, 2020

Now 360

@pchaigno
Copy link
Collaborator

@pchaigno pchaigno commented Mar 24, 2020

Those 360 files make up 27 repositories by 19 users. So it looks like this is growing, albeit very slowly. I'm going to close this issue, but don't hesitate to ping me to reopen if you think we've reached the required threshold of hundreds of repositories.

@pchaigno pchaigno closed this Mar 24, 2020
@ice1000
Copy link
Author

@ice1000 ice1000 commented Apr 3, 2020

Now 406

@pchaigno
Copy link
Collaborator

@pchaigno pchaigno commented Apr 3, 2020

@ice1000 It's good that you're keeping an eye on the number of files, but I don't think it's very useful to post it here unless the number of repositories significantly went up (e.g., +100) or the number of files itself went up (e.g., +1000).

@ice1000
Copy link
Author

@ice1000 ice1000 commented Apr 3, 2020

Ok

@ice1000
Copy link
Author

@ice1000 ice1000 commented Apr 3, 2020

How do I count the repositories? Is there an API?

@pchaigno
Copy link
Collaborator

@pchaigno pchaigno commented Apr 3, 2020

You can use Harvester.

@hwdef hwdef mentioned this pull request May 14, 2020
4 tasks
@ice1000
Copy link
Author

@ice1000 ice1000 commented Aug 25, 2021

@ice1000 It's good that you're keeping an eye on the number of files, but I don't think it's very useful to post it here unless the number of repositories significantly went up (e.g., +100) or the number of files itself went up (e.g., +1000).

May I assume that 1000 files suffice for a new PR (since I failed to make harvester work so I cannot count repos)? It's 760+ files now, and I'm thinking about creating a new PR once it's 1000+.

@lildude
Copy link
Member

@lildude lildude commented Aug 26, 2021

May I assume that 1000 files suffice for a new PR (since I failed to make harvester work so I cannot count repos)? It's 760+ files now, and I'm thinking about creating a new PR once it's 1000+.

No. That is a bad assumption to make. One :user/:repo with 1000 files indicates it is only used by one user. 1000 unique :user/:repo with a single file in each indicates it is widely used. It's the latter that we need.

@Alhadis
Copy link
Collaborator

@Alhadis Alhadis commented Aug 26, 2021

since I failed to make harvester work so I cannot count repos

I'm working on fixing that. Sorry about the inconvenience.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants