Rewriting scripts/lean-pr-testing-comments.sh in JavaScript

Stream: general

[Nick Decroos]

The TODO here says:

The whole script ought to be rewritten in javascript, to avoid having to use curl for API calls.

I'd like to work on this task. Searching through Zulip and the PR's, it seems that nobody is yet working on this.

One issue is that such a script is hard to test.
Should the script work without installing libraries? The script should run in CI, not from command line. I assume I can add depencies in the environment, like npm install axios.

[Michael Rothgang]

A possibly naive question from the sideline: why Javascript? Right now, mathlib's infrastructure is a wild mix of (some) Lean, Python (some scripts, some style linters), Shell (more scripts), Rust (for the cache etc.) - I'm not aware of any Javascript so far. Is there a reason it cannot be rewritten in Lean (or perhaps Rust)?

[Michael Rothgang]

That said: I don't have any horse in this race; I'm not volunteering to rewrite this, but you are - so feel free to ignore my 2c!

[Ruben Van de Velde]

There's some JavaScript in GitHub actions, because that's the one alternative I found for shell scripts

[Bryan Gin-ge Chen]

I'm just now looking at the script and where it's used for the first time, but my impression is that using a shell script is fine for this. If we really want to avoid curl, maybe using the gh CLI tool instead would make it simpler (though maybe that's not installed by default on our runners yet).

[Nick Decroos]

Good remark on using languages that are already used in the infrastrcture and not introducing another language.
I didn't make the TODO, but it mentions that curl should be avoided. I am not sure why curl should be avoided.
It should be possible in Python and Rust. (It should also be possible in Lean using Http I think, but needs more work).

[Bryan Gin-ge Chen]

cc: @Kim Morrison

[Damiano Testa]

I remember various discussions about some systems having very old (or very unusual) versions of curl: maybe this was the origin of the issue?

[Bryan Gin-ge Chen]

Since this particular script is only meant to be run in CI, that should be less of a concern.

[Bryan Gin-ge Chen]

Ah, perhaps the idea was to convert the shell script into something written using the github-script action in the build.yml workflow files?

[Nick Decroos]

I think I should wait for a reaction by @Kim Morrison reacts, before doing anything.

[Kim Morrison]

Yes, it's just a desire to use github-script where possible, to reduce marginally the amount of shell scripting we have interacting with the Github API.

[Kim Morrison]

Looking back at it I'm less convinced that increasing the amount of javascript in our system is a good idea!

[Kim Morrison]

Generally making CI scripts more self-explanatory, better documented, or using more robust APIs is a good idea. But this TODO per se is not really doing that.