expln / metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
https://expln.github.io/lamp/latest/index.html
MIT License
12 stars 5 forks source link

More fix compilation warnings #122

Closed billh0420 closed 1 year ago

billh0420 commented 1 year ago

A) On line 4 of src/rescript-utils/main/Expln_utils_common.res:

     let clearArray:array<'a> => unit = %raw(`arr => arr.length = 0`)

Note: I am not sure why the correct function type is not inferred. I did a google search and it seems that the problem is known and the recommended solution was to use "ignore" to ignore the "return" value. But the ignore has to be placed where it is called (and this also removes the warning). I chose to explicitly specify the return type so that the caller need not worry about it. I didn't check whether something is really returned (the code itself doesn't return anything but rescript might do something).

I can check further, but I am still learning rescript and I would not be sure that I would be doing it correctly.

If the above is not correct, I think there is only one place where this function is called and it is easy enough to add "-> ignore".

B) On lines 33 and 54 and elsewhere of src/metamath/mm-utils/MM_proof_tree.res:

    proofNodeDbg: option<proofNodeDbg>,

    proofTreeDbg: option<proofTreeDbg>,

I made the changes and I can submit a pull request if you wish.

expln commented 1 year ago

Hi billh0420,

Yes, please, submit a PR. Please use shorter names: pnDbg and ptDbg. I use everywhere in MM_proof_tree pn for proofNode and pt for proofTree

expln commented 1 year ago

I didn't check whether something is really returned (the code itself doesn't return anything but rescript might do something).

I think it will be safe to use the type array<'a> => unit as you've done as soon as the compiler output (generated JS code) is not changed after adding this type.

expln commented 1 year ago

Thank you billh0420! I merged your PR.