search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

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

Open briangmilnes opened 2 months ago

briangmilnes commented 2 months ago

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

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 commented 2 months ago

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 commented 2 months ago

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

briangmilnes commented 2 months ago

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 https://github.com/FStarLang/FStar/issues/3469#issuecomment-2346453252, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACKMDK5Y5PB72L5CZR4WH3DZWGP4PAVCNFSM6AAAAABODIMXI2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGNBWGQ2TGMRVGI . You are receiving this because you authored the thread.Message ID: @.***>