search

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

Fix compilation warning 44 #125

Closed billh0420 closed 1 year ago

billh0420 commented 1 year ago

Since we are using version 10.1.4+ of rescript, there is no need to have an alias for 'promise'.

You can check on there web page at https://rescript-lang.org/docs/manual/latest/promise:

Since 10.1 In ReScript, every JS promise is represented with the globally available promise<'a> type. For ReScript versions < 10.1, use its original alias Js.Promise.t<'a> instead.

To eliminate the warning 44, the following changes need to be made:

A) delete line 1 of the file src/rescript-utils/main/Expln_utils_promise.resi:

       type promise<'a> = Js.Promise.t<'a>

B) delete the corresponding line from src/rescript-utils/main/Expln_utils_promise.resi

C) Change line 25 of the file src/metamath/worker/MM_wrk_unify.resi from:

       ) => Expln_utils_promise.promise<MM_proof_tree_dto.proofTreeDto>

to:

      ) => promise<MM_proof_tree_dto.proofTreeDto>

If you wish, I can submit a pull request.

expln commented 1 year ago

I didn't expected that fixing this type of warnings with promises will be such simple (however, I didn't investigate this problem either). Yes, please submit a PR. And thanks for providing detailed explanations of your changes. If it will be easier for you, in similar cases, you may submit a PR first, so you will not need to explain changes in words, I will see them in the diff. Of course, I don't promise that I will merge the PR in such case, but if it will be easier for you why not.

expln commented 1 year ago

Thank you billh0420! I merged your PR.