User avatar
Liam O'Connor @liamoc@types.pl
2mo
I find the proposed agda contributors policy to be quite disappointing. I'm not sure what I will do about this yet, and I'm not actively using Agda at the moment so i don't need to come to a decision now, but I'm leaning towards avoiding Agda as I currently avoid Lean (despite the fact that I like Lean quite a lot as a language, the dreaded bots have infected too much of its ecosystem and culture for me to have a good time engaging with it)
2
0
1
0
User avatar
mio @mio@shrimp.mio19.uk
1mo
@liamoc Where can I read the proposed agda contributors policy? I am unable to find it by using search engines
1
0
0
0
User avatar
Liam O'Connor @liamoc@types.pl
1mo
@mio it's in a pull request, but mostly it's in the context of several issues trying to hash this out. Many people wanted to ban LLM contributions entirely, but out of deference to specific senior members of the dev team who had a different opinion, a completely non-committal policy was instead adopted.
1
0
1
0
User avatar
Liam O'Connor @liamoc@types.pl
1mo
@mio proposed, i guess it hasn't been adopted formally yet
0
0
1
0