master, last three releases all build but can't compile FStar.Common.fst* from emacs or command line

[briangmilnes]

/home/milnes/contrib/multicache/FStar/src/basic/FStar.Common.fst(54,27-57,27):

• Computed type Prims.int & 'b
  and effect FStar.Compiler.Effect.ALL
  is not compatible with the annotated type Prims.int & 'b
  and effect Tot

So we have the issue that this does compile during build but won't compile in a language
server (using it's own fstar.exe). Nor will a command line compile from emacs work.

This prevents me from hacking the system.

I checked for a hung language server and so on.

[nikswamy]

The F* compiler itself builds with a flag called --MLish which sets the default effect to ML, which is different than ordinary F* builds. Do you have this option set?

[briangmilnes]

Ah it's all --MLish! I'll document in my modifying the compiler writeup.

[briangmilnes]

Nik, I did not, it took a while to find it. I was rather amazed that it changed a Tot type in FStar.Common to an effect. I found it, can work in the compiler, have adjusted Forge to allow it (it switches between opam, everest, and a contrib setup already) and closed the issue before you commented. I'll doc it in my MODIFY.md. -B

…

On Thu, Sep 12, 2024 at 7:25 AM nikswamy ***@***.***> wrote: The F* compiler itself builds with a flag called --MLish which sets the default effect to ML, which is different than ordinary F* builds. Do you have this option set? — Reply to this email directly, view it on GitHub <#3469 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACKMDK5Y5PB72L5CZR4WH3DZWGP4PAVCNFSM6AAAAABODIMXI2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGNBWGQ2TGMRVGI> . You are receiving this because you authored the thread.Message ID: ***@***.***>