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

Question on suppressed warning 45 #141

Closed billh0420 closed 1 year ago

billh0420 commented 1 year ago

The warning 45 is being suppressed. Warning 45 is: "Open statement shadows an already defined label or constructor."

The Rescript documentation suggests: "Use open this sparingly, it's convenient, but makes it hard to know where some values come from." They recommend: "You should usually use open in a local scope: ..."

I am looking into not suppressing the warning 45 and fixing the code so that the warning doesn't occur.

As you are probably aware, there are many warnings 45. I don't want to spend time on this if you are not interested in handing this problem.

The following is an example fix for the file MM_cmp_context_selector.res:

A) Delete line 8 which says: "open MM_wrk_settings"

B) Change line 415 from:

    let srcDtoToFileSrc = (~src:mmCtxSrcDto, ~webSrcSettings:array<webSrcSettings>):mmFileSource => {

to:

    let srcDtoToFileSrc = (~src:mmCtxSrcDto, ~webSrcSettings:array<MM_wrk_settings.webSrcSettings>):mmFileSource => {

C) Change line 439 from:

    ~webSrcSettings:array<webSrcSettings>,

to:

     ~webSrcSettings:array<MM_wrk_settings.webSrcSettings>,

D) Change line 483 from:

     ~webSrcSettings:array<webSrcSettings>,

to:

     ~webSrcSettings:array<MM_wrk_settings.webSrcSettings>,

That is, delete the "open" statement causing the conflict and qualify the item being opened.

Are you interested in me pursuing this and submitting such changes? I am not sure if all warnings 45 can be eliminated in such a manner.

The conflict is due to the following two items from MM_wrk_settings and MM_wrk_editor:

  type webSrcSettings = {
      alias: string,
      url: string,
      trusted: bool,
 }

and

type webSource = {
      alias:string,
      url:string,
 }
expln commented 1 year ago

To be honest, I don't want to fix this warning by prepending types with their module names, because this makes the code more verbose. In general, I don't consider this warning a problem. Neither it causes any technical problems in the sense that program will do not what it was expected to do. The compiler will always show an error in such a case. Nor it makes the code less readable, because if you open it in VS Code and if everything compiles without errors then you can navigate to any definition of any type, variable, and function by Ctrl+click on it. I know that not following advices of the language developers might be not a good idea. But I've been programming in ReScript for almost a year (not a long time, though :) ), and I am still not convinced that I should prefer local "opens". Probably this is due to I know everything in the mm-lamp code (except those things which I forgot :) ). But as I mentioned, VS Code has pretty decent capabilities of navigating inside a project which compiles without errors, so this should help to those who are new to the project.

Do you see any significant issues this warning causes?

billh0420 commented 1 year ago

I don't see any significant issues caused with this warning.

I just wanted to see if you wanted this warning eliminated before I spent time working on it.

expln commented 1 year ago

I don't see any significant issues caused with this warning.

Good.

Ok, let's then leave this warning suppressed, at least for now.