Skip to content

Mutind derive param1 - #1060

Merged
gares merged 1 commit into
masterfrom
mutind-derive-param1
Jul 2, 2026
Merged

Mutind derive param1#1060
gares merged 1 commit into
masterfrom
mutind-derive-param1

Conversation

@gares

@gares gares commented Jul 1, 2026

Copy link
Copy Markdown
Contributor

No description provided.

@gares
gares force-pushed the mutind-derive-param1 branch 3 times, most recently from 7568412 to 964bbe4 Compare July 1, 2026 20:48
@gares

gares commented Jul 1, 2026

Copy link
Copy Markdown
Contributor Author

I will proceed like this: I make a PR with just the changes to 1 derivation taken from #1056 in topological order.
It worked fine for the first one I picked, namely param1.
I cleaned up the code generated by LLM quite a bit.

@Janno maybe you could try to give your agent this param1.elpi and the one he generated in #1056 and ask to do the same cleanup on param2.elpi (and the other files). Just tell me, so that I wait for it before moving to the next file

@gares
gares force-pushed the mutind-derive-param1 branch from 964bbe4 to 281bb7f Compare July 1, 2026 21:04
@gares
gares merged commit d338452 into master Jul 2, 2026
133 of 137 checks passed
@gares
gares deleted the mutind-derive-param1 branch July 2, 2026 08:45
@Janno

Janno commented Jul 6, 2026

Copy link
Copy Markdown
Contributor

@Janno maybe you could try to give your agent this param1.elpi and the one he generated in #1056 and ask to do the same cleanup on param2.elpi (and the other files). Just tell me, so that I wait for it before moving to the next file

Sorry, I was busy with Rocq'n'share last week. I'll start working on this.

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.

2 participants