CakeML
Constant propagation in word_simp
At the moment, constant foldng/propagation in wordLang is limited to expressions:
https://github.com/CakeML/cakeml/blob/master/compiler/backend/word_simpScript.sml#L156
This issue is about extending it to work for instructions as well:
https://github.com/CakeML/cakeml/blob/master/compiler/backend/word_simpScript.sml#L220
(and probably other simple places that could benefit).
This was reported by @talsewell in the context of Pancake programs.
For the purposes of pancake programs, this might be fixed by https://github.com/CakeML/cakeml/pull/1169 , assuming that PR succeeds.
Hi! I’d like to work on this issue. Could you please assign it to me?
Hi! I’d like to work on this issue. Could you please assign it to me?
Sure, do you have some background in HOL4 / CakeML, or are you working with someone who is involved in CakeML dev? I'm afraid it would be a bit difficult to do this from scratch without guidance.
I don’t have any prior background in HOL4 or CakeML, and I’m not working with anyone directly involved in CakeML development. I’m new to this area and would really appreciate some guidance on how to get started, or suggestions for beginner-friendly issues I could look at.
It might be good to go here: https://hol-theorem-prover.org/ and get started with picking up HOL first (check out Tutorial and Documentation, and also join the Zulip community for help).
As for this issue, it will probably be assigned to one of my students (soon).
Thank you for the guidance. I’ll go through the HOL tutorial and documentation from the official site, and also join the Zulip community to get a better understanding. I understand this issue will likely be assigned to someone else, and that’s perfectly fine — I’ll focus on learning the basics first before trying to contribute further