Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Officially support building F* from source with F# 4.1 #1358

Closed
ranweiler opened this issue Dec 15, 2017 · 33 comments
Closed

Officially support building F* from source with F# 4.1 #1358

ranweiler opened this issue Dec 15, 2017 · 33 comments

Comments

@ranweiler
Copy link

ranweiler commented Dec 15, 2017

Summary

It seems like this is mostly working already. There is some discussion of this in the comments of #878, but it seemed worth breaking this out into its own issue. Presumably it also needs systematic assessment on all supported operating systems.

This did not work for me out of the box. I'd like to share what I needed to do to build F* from scratch, and hopefully we can figure out if (a) my workarounds were ultimately unnecessary, and the docs can simply be updated to claim F# 4.1 support, or (b) if the build configuration should be tweaked.

In short: most things work, but someone with more context should glance at the minor issues I came across.

There were 3 problems I ran into.

  1. Executable format assumptions
  2. Targeted version of FSharp.Core
  3. Successfully running all example benchmarks

I'll address each of these below. I may refer to the numbered build-from-source steps in INSTALL.md. Note that I only ran into issues with Step 1 of those instructions.

Platform and versions

This was building the latest master (b8ea92f).

I'm running x86-64 Void Linux (kernel 4.14.5), using Mono with no prior F# or F* installs (i.e. no DLLs hanging around from previous F# versions). Specifically, I built F* with:

  • F# 4.1.0.2
  • Mono 5.4.1.6
  • opam 1.2.2
  • OCaml 4.02.3
  • Z3 4.5.0

1. Executable format assumptions

This a somewhat trivial documentation issue. If a Linux user has Mono installed, but the CLR binary format has not been registered as an executable format, the default F* instructions for Step 1 to test the correctness of the executable do not work verbatim (unsurprisingly!). On Linux, to run a CLR executable, one can either generally use shim scripts that call e.g. mono fstar.exe, or tell the kernel about the CLR format, as described here. For building F* from source, I chose the latter.

I believe this is done by default when installing mono-complete on Debian (at least if the Apt::Install-Recommends config value is set to something truthy), but I haven't tested it. On Void, this requires explicit opting-in per the instructions I just linked to. Due to the non-portability of this solution, the F* team may want to punt this to users to address as they see fit, which is valid. If so, it would be helpful to comment on this in the build docs. Otherwise, it might be nice to add shim scripts/test symlinks for Step 1 builds, which always do the right thing. I'd personally suggest the former for now.

2. Target F# Core version

This issue is more substantive, and a place where I lack context.

Throughout the project, there is a configuration value named TargetFSharpCoreVersion, set to 4.4.0.0. If I build F* from sources using make -C src, then I observe the following warnings:

...
Configuration: Release Platform: AnyCPU
/usr/lib/mono/xbuild/14.0/bin/Microsoft.Common.targets:  warning : Reference 'FSharp.Core, Version=4.4.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' not resolved
Configuration: Release Platform: AnyCPU
/usr/lib/mono/xbuild/14.0/bin/Microsoft.Common.targets:  warning : Reference 'FSharp.Core, Version=4.4.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' not resolved
Configuration: Release Platform: AnyCPU
/usr/lib/mono/xbuild/14.0/bin/Microsoft.Common.targets:  warning : Reference 'FSharp.Core, Version=4.4.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' not resolved
Configuration: Release Platform: AnyCPU
/usr/lib/mono/xbuild/14.0/bin/Microsoft.Common.targets:  warning : Reference 'FSharp.Core, Version=4.4.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' not resolved
Configuration: Release Platform: AnyCPU
/usr/lib/mono/xbuild/14.0/bin/Microsoft.Common.targets:  warning : Reference 'FSharp.Core, Version=4.4.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' not resolved
/home/joe/src/FStar/src/typechecker/FStar.TypeChecker.DMFF.fs(572,9): warning FS0025: Incomplete pattern matches on this expression. For example, the value 'Tm_ascribed (_, (_,Some (_)), _)' may indicate a case not covered by the pattern(s).
Configuration: Release Platform: AnyCPU
/usr/lib/mono/xbuild/14.0/bin/Microsoft.Common.targets:  warning : Reference 'FSharp.Core, Version=4.4.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' not resolved
Configuration: Release Platform: AnyCPU
/usr/lib/mono/xbuild/14.0/bin/Microsoft.Common.targets:  warning : Reference 'FSharp.Core, Version=4.4.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' not resolved
Configuration: Release Platform: AnyCPU
/usr/lib/mono/xbuild/14.0/bin/Microsoft.Common.targets:  warning : Reference 'FSharp.Core, Version=4.4.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' not resolved
Configuration: Release Platform: AnyCPU
/usr/lib/mono/xbuild/14.0/bin/Microsoft.Common.targets:  warning : Reference 'FSharp.Core, Version=4.4.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' not resolved
Configuration: Release Platform: AnyCPU
/usr/lib/mono/xbuild/14.0/bin/Microsoft.Common.targets:  warning : Reference 'FSharp.Core, Version=4.4.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' not resolved
Configuration: Release Platform: AnyCPU
/usr/lib/mono/xbuild/14.0/bin/Microsoft.Common.targets:  warning : Reference 'FSharp.Core, Version=4.4.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' not resolved
...

This led me to expect some sort of runtime failure. Indeed, if I try to run the freshly-built CLR executable to check it, I observe.

$ ./bin/fstar.exe
Can't find custom attr constructor image: /home/joe/src/FStar/bin/FSharp.Compatibility.OCaml.dll mtoken: 0x0a000001 due to: Could not load file or assembly 'FSharp.Core, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' or one of its dependencies. assembly:FSharp.Core, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a type:<unknown type> member:<none>
Unhandled Exception:
System.TypeInitializationException: The type initializer for '<StartupCode$basic>.$FStar.Util' threw an exception. ---> System.BadImageFormatException: Could not resolve field token 0x0400007b
  at <StartupCode$basic>.$FStar.Util..cctor () [0x0007b] in <5a333f43864a5396a7450383433f335a>:0
   --- End of inner exception stack trace ---
  at (wrapper managed-to-native) System.Object:__icall_wrapper_mono_generic_class_init (intptr)
  at FStar.Util.print1_error (System.String a, System.String b) [0x00013] in <5a333f43864a5396a7450383433f335a>:0
  at FStar.Main.main[a] () [0x0006a] in <5a335536ce2aad61a74503833655335a>:0
  at FStar.Top+t@6-1.Invoke () [0x00001] in <5a335536ce2aad61a74503833655335a>:0
  at System.Threading.ThreadHelper.ThreadStart_Context (System.Object state) [0x00014] in <a1a24c57c20a404fb15a014686964947>:0
  at System.Threading.ExecutionContext.RunInternal (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state, System.Boolean preserveSyncCtx) [0x00071] in <a1a24c57c20a404fb15a014686964947>:0
  at System.Threading.ExecutionContext.Run (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state, System.Boolean preserveSyncCtx) [0x00000] in <a1a24c57c20a404fb15a014686964947>:0
  at System.Threading.ExecutionContext.Run (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state) [0x0002b] in <a1a24c57c20a404fb15a014686964947>:0
  at System.Threading.ThreadHelper.ThreadStart () [0x00008] in <a1a24c57c20a404fb15a014686964947>:0
[ERROR] FATAL UNHANDLED EXCEPTION: System.TypeInitializationException: The type initializer for '<StartupCode$basic>.$FStar.Util' threw an exception. ---> System.BadImageFormatException: Could not resolve field token 0x0400007b
  at <StartupCode$basic>.$FStar.Util..cctor () [0x0007b] in <5a333f43864a5396a7450383433f335a>:0
   --- End of inner exception stack trace ---
  at (wrapper managed-to-native) System.Object:__icall_wrapper_mono_generic_class_init (intptr)
  at FStar.Util.print1_error (System.String a, System.String b) [0x00013] in <5a333f43864a5396a7450383433f335a>:0
  at FStar.Main.main[a] () [0x0006a] in <5a335536ce2aad61a74503833655335a>:0
  at FStar.Top+t@6-1.Invoke () [0x00001] in <5a335536ce2aad61a74503833655335a>:0
  at System.Threading.ThreadHelper.ThreadStart_Context (System.Object state) [0x00014] in <a1a24c57c20a404fb15a014686964947>:0
  at System.Threading.ExecutionContext.RunInternal (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state, System.Boolean preserveSyncCtx) [0x00071] in <a1a24c57c20a404fb15a014686964947>:0
  at System.Threading.ExecutionContext.Run (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state, System.Boolean preserveSyncCtx) [0x00000] in <a1a24c57c20a404fb15a014686964947>:0
  at System.Threading.ExecutionContext.Run (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state) [0x0002b] in <a1a24c57c20a404fb15a014686964947>:0
  at System.Threading.ThreadHelper.ThreadStart () [0x00008] in <a1a24c57c20a404fb15a014686964947>:0

Note Could not load file or assembly 'FSharp.Core, Version=4.0.0.0.

To fix this, I used a very crude solution. If I run grep -F '4.4.0.0' -R ., I can find various occurrences of this version string in TargetFSharpCoreVersion XML configuration values. I did a find/replace to change every such occurrence of 4.4.0.0 with 4.4.1.0, per this guide. This build succeeded, and I was able to run the fstar.exe --version, as well as various sub-projects in the examples directory.

There may be a much better solution. For example:

  1. It may be sufficient to just ensure that the developer has certain header files (when building) and DLLs (when executing), even if using F# 4.1 to build. This may also be preferable, and it may be a quirk of my system that they aren't readily available. My distro errs on the side of more minimal packaging; on Debian or Ubuntu, the fix may just be an apt-get away.
  2. Maybe only some occurrences of TargetFSharpCoreVersion need to be updated, or maybe it is enough to update the bindingRedirect value I see in some config files (which I in fact never edited).

My background is Unix, not Windows/the CLR, so I very much defer to others here. I assume that my heavy-handed first guess of a solution is the wrong one.

3. Successfully running all example benchmarks

I was able to run most projects in examples/, as I mentioned, as well as perform OCaml code extraction and rebuild the F* compiler from freshly-extracted OCaml (steps 2 and 3 of INSTALL.md).

However, one of the microbenchmark make targets failed (all-neg). The expectation for NEGTESTS was 39, but I locally produced 40 failures. I don't know if this is related to my experimentation with the build config, a CLR/CLR lib issue, a quirk of the Z3 version I'm using, a real regression in master, or a fluke of some other sort. If needed, I can open a new issue for it with more detail. If it is a dubious or flexible expectation in the first place, that would be helpful to know (and perhaps document).

Thanks!

@catalin-hritcu
Copy link
Member

@ranweiler Many thanks for the detailed report. Some quick answers:

  1. I think your assessment is right and we should document this properly.
  2. Could not reproduce this problem with Arch Linux, mono, and fsharp 4.1.23. I don't see the warnings and I don't get the error.
  3. Could reproduce this one, but I don't think it has anything to do with the precise F# version. It's more about the F# version of F* still lagging behind the OCaml one. Despite recent progress by @A-Manning, it seems it's still behind? Maybe @A-Manning can clarify what to expect.

I guess you're aware that Step 1 from INSTALL.md (building via F#) is not required, you can also bootstrap F* completely in OCaml, using an old F* version extracted to OCaml (Steps 2-3).

@ranweiler
Copy link
Author

@catalin-hritcu Thanks! I did notice that Step 1 can be skipped— I just figured I'd use myself as a test case for building from scratch on Linux.

  1. Great! I can submit a PR for that to move things along.

  2. Interesting. Before opening this issue, I had noticed that you had success in F* fails to build with F# from source #878, as described here. My only worry was that, since you described your distro as updating the F# version, the assembly for FSharp.Core 4.4.0.0 might be lingering on your system, and would thus be discoverable by xbuild/the Mono runtime. This would then be unlike my (fresh) system, where the first and only version of F# that I've installed is 4.1, so I'd lack the "legacy" 4.4.0.0 version of FSharp.Core. Checking, I do see the following:

    $ mono-api-info /usr/lib/mono/fsharp/FSharp.Core.dll  | grep '<assembly'
      <assembly name="FSharp.Core" version="4.4.1.0">
    

    Could you check on your system, and see if you indeed have an assembly for 4.4.0.0?

    Since my understanding is that FSharp.Core 4.4.0.0 should be binary compatible with 4.4.1.0, it would make sense to continue targeting a lower version for the sake of broader compatibility.

    I guess I'd expect my newer version of FSharp.Core to still work, due to alleged binary compatibility, but that might require a change to the build config. My expectations might also just be incorrect. I'm basically brand-new to the CLR, so I defer to others/seek advice here.

  3. I see. I captured the output of my "bad" run, and can share that to diff against a good one if desired. I'll note that I just double-checked, and can reproduce this failure with both the Step 1 and Step 3 builds of fstar.exe.

@catalin-hritcu
Copy link
Member

catalin-hritcu commented Dec 16, 2017

  1. I get the same output from the command you suggested:
$ mono-api-info /usr/lib/mono/fsharp/FSharp.Core.dll  | grep '<assembly'
  <assembly name="FSharp.Core" version="4.4.1.0">

In case it helps narrow this down, here is a what I get on a clean F# build on a clean repo:
https://gist.github.com/catalin-hritcu/4914dab50512b257729a22a6071fa017

  1. Right, I can also reproduce this problem (40 failures) with the OCaml build. Seems like a Windows vs Linux issue, since our Windows CI machine seems to work well (39 failures):
    https://raw.githubusercontent.com/project-everest/ci-logs/master/fstar-ci-988b1f2f-15127.all
    The output is super verbose, so it's hard to detect the source of the problem even after editing my output to remove some of the irrelevant diffs.
    mine.txt
    ci.txt

@catalin-hritcu
Copy link
Member

catalin-hritcu commented Dec 16, 2017

  1. Actually not a Windows vs Linux thing. Even my Windows VM fails with 40 failures. So I have no clue how the CI machine can be succeeding.

Finally managed to narrow this down: on all my machines NegativeTests.ZZImplicitFalse.fst causes 2 errors

.\NegativeTests.ZZImplicitFalse.fst(4,0-4,33): (Error 19) assertion failed(Also see: E:\Projects\fstar\pub\ulib\prims.fst(205,30-205,42))
.\NegativeTests.ZZImplicitFalse.fst(4,26-4,27): (Error 65) Failed to resolve implicit argument of type 'Prims.l_False' introduced in (*?u1*) _ uu___56

But on the CI machine it causes only the 2nd error, but not the 1st "assertion failed" pointing at prims.fst.

@catalin-hritcu
Copy link
Member

Thanks to @mtzguido we narrowed 3 to the --use_two_phase_tc true that's now passed in from the top-level Makefile in examples, but which is currently not the default. This is quite shady since it makes our instructions for testing a binary package not work for instance:
https://github.com/FStarLang/FStar/blob/master/INSTALL.md#testing-a-binary-package
We're looking for a fix.

@ranweiler
Copy link
Author

ranweiler commented Dec 16, 2017

Thanks for that build output on (2), @catalin-hritcu! Once difference that I see immediately is that your invocation of make uses msbuild, which is in your path, while mine fails to find it and uses the deprecated xbuild from Mono. Since the build scripts warn that xbuild is deprecated, I'll work toward getting a successful Step 1 build using msbuild. (Maybe it is time to disclaim any support for xbuild?)

To get msbuild, I installed the dotnet tools from https://github.com/dotnet/core. This exposes msbuild as a subcommand of dotnet. I then added a shim shell script named msbuild to my $PATH with the body dotnet msbuild "$@".

Showing the versions I'm working with:

$ dotnet --version
2.0.3

$ msbuild /version
Microsoft (R) Build Engine version 15.4.8.50001 for .NET Core
Copyright (C) Microsoft Corporation. All rights reserved.
15.4.8.50001

Then, when i invoke make -C src, I get:

$ make -C src
make: Entering directory '/home/joe/src/FStar/src'
mono VS/.nuget/NuGet.exe restore VS/FStar.sln
All packages listed in packages.config are already installed.
make -C VS install-packages
make[1]: Entering directory '/home/joe/src/FStar/src/VS'
[ -d packages ] || make update-nuget
mono .nuget/NuGet.exe restore FStar.sln
All packages listed in packages.config are already installed.
find packages -name '*.exe' -exec chmod +x '{}' ';'
make[1]: Leaving directory '/home/joe/src/FStar/src/VS'
/home/joe/bin/msbuild /verbosity:minimal /p:Configuration=Release VS/FStar.sln
Microsoft (R) Build Engine version 15.4.8.50001 for .NET Core
Copyright (C) Microsoft Corporation. All rights reserved.
/home/joe/src/FStar/src/basic/basic.fsproj : error MSB4057: The target "Build" does not exist in the project.
/home/joe/src/FStar/src/smtencoding/smtencoding.fsproj(55,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/fsdoc/fsdoc.fsproj(60,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/prettyprint/prettyprint.fsproj(55,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/tosyntax/tosyntax.fsproj : error MSB4057: The target "Build" does not exist in the project.
/home/joe/src/FStar/src/reflection/reflection.fsproj(96,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/tests/tests.fsproj(58,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/tactics/tactics.fsproj(123,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/syntax/syntax.fsproj(53,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/extraction/extraction.fsproj(52,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/typechecker/typechecker.fsproj(54,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/format/format.fsproj : error MSB4057: The target "Build" does not exist in the project.
/home/joe/src/FStar/src/parser/parser.fsproj : error MSB4057: The target "Build" does not exist in the project.
/home/joe/src/FStar/src/fstar/fstar.fsproj : error MSB4057: The target "Build" does not exist in the project.
make: *** [Makefile:18: fstar-in-fsharp] Error 1
make: Leaving directory '/home/joe/src/FStar/src'

I notice in your build output you have Microsoft (R) Build Engine version 15.2.0.0 , which I'm guessing is the discrepancy. I'll (1) try to get an older version of msbuild that matches yours, then re-test, and (2) try to determine what it might take to update the existing build to work with msbuild 15.4 in a backwards-compatible way. My sense is that we really want 15.4 to work out of the box, as it seems to be the latest stable version (I'm not sure how this relates to the build tooling that powers the various IDEs). What's the project philosophy here?

P.S. nice investigating on (3)! If other folks are relying on CI to run tests, that would explain why this hasn't been caught yet.

@ranweiler
Copy link
Author

Note: when I try to build with the newer msbuild, the specific failure output I get looks like this:

$ make -C src
make: Entering directory '/home/joe/src/FStar/src'
mono VS/.nuget/NuGet.exe restore VS/FStar.sln
All packages listed in packages.config are already installed.
make -C VS install-packages
make[1]: Entering directory '/home/joe/src/FStar/src/VS'
[ -d packages ] || make update-nuget
mono .nuget/NuGet.exe restore FStar.sln
All packages listed in packages.config are already installed.
find packages -name '*.exe' -exec chmod +x '{}' ';'
make[1]: Leaving directory '/home/joe/src/FStar/src/VS'
/home/joe/bin/msbuild /verbosity:minimal /p:Configuration=Release VS/FStar.sln
Microsoft (R) Build Engine version 15.4.8.50001 for .NET Core
Copyright (C) Microsoft Corporation. All rights reserved.
/home/joe/src/FStar/src/basic/basic.fsproj : error MSB4057: The target "Build" does not exist in the project.
/home/joe/src/FStar/src/smtencoding/smtencoding.fsproj(55,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/fsdoc/fsdoc.fsproj(60,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/prettyprint/prettyprint.fsproj(55,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/tosyntax/tosyntax.fsproj : error MSB4057: The target "Build" does not exist in the project.
/home/joe/src/FStar/src/syntax/syntax.fsproj(53,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/tactics/tactics.fsproj(123,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/extraction/extraction.fsproj(52,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/tests/tests.fsproj(58,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/reflection/reflection.fsproj(96,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
/home/joe/src/FStar/src/format/format.fsproj : error MSB4057: The target "Build" does not exist in the project.
/home/joe/src/FStar/src/fstar/fstar.fsproj : error MSB4057: The target "Build" does not exist in the project.
/home/joe/src/FStar/src/parser/parser.fsproj : error MSB4057: The target "Build" does not exist in the project.
/home/joe/src/FStar/src/typechecker/typechecker.fsproj(54,3): error MSB4020: The value "" of the "Project" attribute in element <Import> is invalid.
make: *** [Makefile:18: fstar-in-fsharp] Error 1
make: Leaving directory '/home/joe/src/FStar/src'

The first error is error MSB4057: The target "Build" does not exist in the project.. I see that the DefaultTargets attributes of Project in the various .fsproj files (e.g. basic.fsproj) always has value "Build". However, I don't see an actual Target tag with Name="Build" anywhere in the project repo (checked via grep '<Target Name="Build"' -R .). Are we relying on the existence of an implicit "Build" target, or the generation of such a target via e.g. the Makefile? I'm wondering if this is something that changed between msbuild versions.

@catalin-hritcu
Copy link
Member

@ranweiler Did some testing and it seems this works with msbuild version 14.1.x-15.2.x. With 15.4 things failed catastrophically for me too: https://gist.github.com/catalin-hritcu/0d69560709e4916c9c31e380ad699449

@ranweiler
Copy link
Author

Debugging further, I'm seeing that when defining FSharpTargetsPath, there are also some path assumptions in the .fsproj files that are false on my particular system. This is the cause of the MSB4020 errors above.

On my system, msbuild computes a value of FSharpTargetsPath = /home/joe/.local/dotnet/sdk/2.0.3/Microsoft/VisualStudio/v/FSharp/Microsoft.FSharp.Targets. I checked this by setting /verbosity:diag in src/Makefile.config and inspecting the output.

However, this path doesn't exist on my system. Instead, the desired file can be found in .local/dotnet/sdk/2.0.3/FSharp/Microsoft.FSharp.Targets. In fact, in the various .fsproj files, FSharpTargetsPath is defined in an inconsistent (sometimes conditional) way. In some project files, we succeed in setting it to a nonexistent path (example), and sometimes we fail to set it because we never satisfy a Condition attribute in the fallthrough case (example), and get an empty string at the variable's use site (example), which triggers the MSB4020 error.

I'm not yet sure about the MSB4057 nonexistent "Build" target errors, but my current hypothesis is that older msbuild versions have an implicit Target with Name="Build" for some (all?) Project tags. I'm curious if there's any hint about that in the diagnostic-level msbuild output for a working msbuild version.

@ranweiler
Copy link
Author

ranweiler commented Dec 16, 2017

@catalin-hritcu oh wow, so your build failures are different than mine, even. It's tough, because on Linux, it seems like there are many, many ways a user could have valid installs of the various tools.

I think it would be nice if a user could just install the latest upstream dotnet release and have things work, but if you have a known good range, I would say support for MSBuild 15.4 should be its own issue, and lower priority. If others really want it, or Hombrew/major Linux distros start packaging it, then it might be worth fiddling with the build some more. WDYT?

@ranweiler
Copy link
Author

Okay, adding to the above comment: it actually seems like MSBuild 15.4 support is important and inevitable, since these tools seems to be moving somewhat fast, and 15.4 is the MSBuild version that comes with the latest stable, non-LTS release of https://github.com/Microsoft/dotnet, as well as Visual Studio 2017 (see here). We really probably don't want the F* build to fail for the latest version of e.g. Visual Studio 2017 / the latest release of the .NET SDK.

Unless someone else "owns" the build code and wants to do it themselves, I can take a stab at this and open a PR, though it will be important to have others review and test it carefully, as I'm new to this whole toolchain.

@A-Manning
Copy link
Contributor

A-Manning commented Dec 17, 2017

Regarding the current state of F* with F# -

F# build of F*

It should be possible to build F* with F#, on both linux and windows. I personally can't merge anything but I'm sure a PR would be welcome if you want to fix building with F# 4.1, @ranweiler.

The F# build uses bigint arithmetic now, like the OCaml build. As far as I'm aware there should not be any issues of unsoundness in F# but not OCaml builds.

The F# build is behind in some minor areas, like unicode support.

Extracted F# code

#1096 is a major roadblock for getting extracted F# code to work. According to @nikswamy it may be possible to remove unused type parameters when extracting, but non-trivial. A patch to the F# compiler that would fix #1096 has been approved-in-principle, and I'm working on this right now. Because of #1096, it's not possible to realise various important parts of ulib in F# - even Prims and Pervasives, IIRC. As a result it is not possible to build ulib when extracting to F#. Your options at the moment are to either use OCaml, or to use a modified F# compiler that allows for unused type parameters when compiling extracted F# code.

There are far more OCaml realised modules for ulib than there are in F#. I think most F# realisations are out of date, as well. Once #1096 is fixed, it's worth taking a look at these and bringing them up-to-date with respect to the OCaml realisations.

Extracted F# code is ugly compared to extracted OCaml. It would be worth working on integrating an F# formatter like Fantomas in order to improve this slightly. Still, Fantomas is not a full solution to this and some additional work is required if we want to have extracted F# looking as good as extracted OCaml.

@ranweiler
Copy link
Author

@A-Manning thanks for the rundown of the current state of F#/F*, having that context is very helpful!

For now, I'll open a PR to support the latest MSBuild release. Since @catalin-hritcu has had success with an older range of MSBuild versions, my sense is that my my PR should be enough to close this issue out, unless we want to fold the CI/local test discrepancy into this issue. However, since that discrepancy also exists on Windows, I'd suggest we make that it's own issue and address it separately.

@catalin-hritcu
Copy link
Member

We're in the process of migrating to VS2017 and F# 4.1 and I have a new branch about that:
https://github.com/FStarLang/FStar/tree/catalin_fsharp-4.1-upgrade

It currently fails Windows CI though:
https://raw.githubusercontent.com/project-everest/ci-logs/master/fstar-ci-cfb8e1bb-19352.all
Does any of you have any ideas about this?

For me this branch works on both Linux and Windows, and for what it's worth it also works on the Linux Nightly machine (although that uses xbuild which is a different beast)

@A-Manning
Copy link
Contributor

A-Manning commented Apr 18, 2018

<Reference Include="FSharp.Core">
<HintPath>..\VS\packages\FSharp.Core.4.2.3/lib/net45/FSharp.Core.dll</HintPath>
<Private>True</Private>
</Reference>

You need to change the references to FSharp.Core.4.2.3 to FSharp.Core.4.3.4 in your .fsproj files.

@catalin-hritcu
Copy link
Member

catalin-hritcu commented Apr 18, 2018

You need to change the references to FSharp.Core.4.2.3 to FSharp.Core.4.3.4 in your .fsproj files.

@A-Manning I'm not an expert on any of this but I managed to get a green on the Windows CI just by reapplying most of your fsproj changes from PR #1404.

If you have further improvements now would be a good time for another pull request against my catalin_fsharp-4.1-upgrade branch.

@ranweiler You also still owe us one? Anything left of that? :)

@ranweiler
Copy link
Author

@catalin-hritcu I'm traveling at the moment, but I'll catch up on this when I get back next week!

@catalin-hritcu
Copy link
Member

@cpitclaudel Is reporting still seeing errors on the catalin_fsharp-4.1-upgrade branch with the latest Ubuntu packages (hope he can report precise version numbers):

FSC : error FS1225: File '/build/fstar/master/bin/FSharp.Core.optdata' not found alongside FSharp.Core. File expected in /build/fstar/master/bin/FSharp.Core.optdata. Consider upgrading to a more recent version of FSharp.Core, where this file is no longer be required. [/build/fstar/master/src/basic/basic.fsproj]
FSC : error FS0229: Error opening binary file '/build/fstar/master/bin/FSharp.Core.dll': The exception has been reported. This internal exception should now be caught at an error recovery point on the stack. Original message: File '/build/fstar/master/bin/FSharp.Core.optdata' not found alongside FSharp.Core. File expected in /build/fstar/master/bin/FSharp.Core.optdata. Consider upgrading to a more recent version of FSharp.Core, where this file is no longer be required.) [/build/fstar/master/src/basic/basic.fsproj]
FSC : error FS3160: Problem reading assembly '/build/fstar/master/bin/FSharp.Core.dll': The exception has been reported. This internal exception should now be caught at an error recovery point on the stack. Original message: Error opening binary file '/build/fstar/master/bin/FSharp.Core.dll': The exception has been reported. This internal exception should now be caught at an error recovery point on the stack. Original message: File '/build/fstar/master/bin/FSharp.Core.optdata' not found alongside FSharp.Core. File expected in /build/fstar/master/bin/FSharp.Core.optdata. Consider upgrading to a more recent version of FSharp.Core, where this file is no longer be required.)) [/build/fstar/master/src/basic/basic.fsproj]
error FS0073 : internal error : BuildFrameworkTcImports: no successful import of /build/fstar/master/bin/FSharp.Core.dll [/build/fstar/master/src/basic/basic.fsproj

@A-Manning @ranweiler Can any of you reproduce this? (I can't.)
Are things working for you with this branch?

@cpitclaudel
Copy link
Contributor

Here:

$ fsharpc
Microsoft (R) F# Compiler version 4.1
$ msbuild 
Microsoft (R) Build Engine version 15.4.0.0 ( Wed Nov 29 14:56:11 UTC 2017) for Mono

@A-Manning
Copy link
Contributor

@cpitclaudel can you paste the output of mono -V?

@cpitclaudel
Copy link
Contributor

$ mono -V
Mono JIT compiler version 5.10.1.20 (tarball Thu Mar 29 10:48:35 UTC 2018)
Copyright (C) 2002-2014 Novell, Inc, Xamarin Inc and Contributors. www.mono-project.com
	TLS:           __thread
	SIGSEGV:       altstack
	Notifications: epoll
	Architecture:  amd64
	Disabled:      none
	Misc:          softdebug 
	Interpreter:   yes
	LLVM:          supported, not enabled.
	GC:            sgen (concurrent by default)

@catalin-hritcu
Copy link
Member

I have the same mono and fsharpc versions, so it's probably not that.

@cpitclaudel
Copy link
Contributor

Maybe I'm doing something wrong? Hmm.

@catalin-hritcu
Copy link
Member

I've upgraded my msbuild to 15.4.0.0 and it still works for me:

$ msbuild /version                                                         (git)-[catalin_fsharp-4.1-upgrade] 
Microsoft (R) Build Engine version 15.4.0.0 ( Wed Nov 29 14:56:11 UTC 2017) for Mono
Copyright (C) Microsoft Corporation. All rights reserved.

$ make                                                                     (git)-[catalin_fsharp-4.1-upgrade] 
mono VS/.nuget/NuGet.exe restore VS/FStar.sln
All packages listed in packages.config are already installed.
make -C VS install-packages
make[1]: Entering directory '/home/hritcu/Projects/fstar/pub/src/VS'
[ -d packages ] || make update-nuget
mono .nuget/NuGet.exe restore FStar.sln
All packages listed in packages.config are already installed.
find packages -name '*.exe' -exec chmod +x '{}' ';'
make[1]: Leaving directory '/home/hritcu/Projects/fstar/pub/src/VS'
/usr/bin/msbuild /verbosity:minimal /p:Configuration=Release VS/FStar.sln
Microsoft (R) Build Engine version 15.4.0.0 ( Wed Nov 29 14:56:11 UTC 2017) for Mono
Copyright (C) Microsoft Corporation. All rights reserved.

/home/hritcu/Projects/fstar/pub/src/basic/boot/NotFStar.Util.fs(50,5): warning FS3190: Lowercase literal 'max_int' is being shadowed by a new pattern with the same name. Only uppercase and module-prefixed literals can be used as named patterns. [/home/hritcu/Projects/fstar/pub/src/basic/basic.fsproj]
  basic -> /home/hritcu/Projects/fstar/pub/bin/basic.dll
  Restoring NuGet packages...
  To prevent NuGet from downloading packages during build, open the Visual Studio Options dialog, click on the Package Manager node and uncheck 'Allow NuGet to download missing packages'.
  prettyprint -> /home/hritcu/Projects/fstar/pub/bin/prettyprint.dll
  parser -> /home/hritcu/Projects/fstar/pub/bin/parser.dll
  syntax -> /home/hritcu/Projects/fstar/pub/bin/syntax.dll
  tosyntax -> /home/hritcu/Projects/fstar/pub/bin/tosyntax.dll
/home/hritcu/Projects/fstar/pub/src/typechecker/FStar.TypeChecker.Tc.fs(1053,15): warning FS0025: Incomplete pattern matches on this expression. [/home/hritcu/Projects/fstar/pub/src/typechecker/typechecker.fsproj]
  typechecker -> /home/hritcu/Projects/fstar/pub/bin/typechecker.dll
  format -> /home/hritcu/Projects/fstar/pub/bin/format.dll
  reflection -> /home/hritcu/Projects/fstar/pub/bin/reflection.dll
  extraction -> /home/hritcu/Projects/fstar/pub/bin/extraction.dll
  fsdoc -> /home/hritcu/Projects/fstar/pub/bin/fsdoc.dll
  smtencoding -> /home/hritcu/Projects/fstar/pub/bin/smtencoding.dll
  tactics -> /home/hritcu/Projects/fstar/pub/bin/tactics.dll
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2057,5): warning MSB3277: Found conflicts between different versions of "FSharp.Core" that could not be resolved.  These reference conflicts are listed in the build log when log verbosity is set to detailed. [/home/hritcu/Projects/fstar/pub/src/fstar/fstar.fsproj]
  fstar -> /home/hritcu/Projects/fstar/pub/bin/fstar.exe
  tests -> /home/hritcu/Projects/fstar/pub/bin/tests.exe
dos2unix parser/parse.fsi
dos2unix: converting file parser/parse.fsi to Unix format...
chmod a+x ../bin/tests.exe
chmod a+x ../bin/fstar.exe

I'm on Arch Linux, which is a bit different from Ubuntu, but can't think of other differences.

@cpitclaudel
Copy link
Contributor

cpitclaudel commented Apr 26, 2018

I just set up a clean VM to experiment. I used Ubuntu 16.04, got mono from http://www.mono-project.com/download/stable/#download-lin-ubuntu, and ran this:

sudo apt-get install mono-complete fsharp
git clone --depth 1 https://github.com/FStarLang/FStar.git -b catalin_fsharp-4.1-upgrade
make -j4 -C FStar/src/

The build goes through, but with warnings:

make: Entering directory '/home/vagrant/FStar/src'
mono VS/.nuget/NuGet.exe restore VS/FStar.sln
Installing 'FSharp.Compatibility.OCaml 0.1.10'.
Installing 'FsLexYacc 6.1.0'.
Installing 'FsLexYacc.Runtime 6.1.0'.
Installing 'PPrintForFSharp 0.0.2'.
Successfully installed 'PPrintForFSharp 0.0.2'.
Successfully installed 'FSharp.Compatibility.OCaml 0.1.10'.
Successfully installed 'FsLexYacc.Runtime 6.1.0'.
Successfully installed 'FsLexYacc 6.1.0'.
make -C VS install-packages
make[1]: Entering directory '/home/vagrant/FStar/src/VS'
[ -d packages ] || make update-nuget
mono .nuget/NuGet.exe restore FStar.sln
All packages listed in packages.config are already installed.
find packages -name '*.exe' -exec chmod +x '{}' ';'
make[1]: Leaving directory '/home/vagrant/FStar/src/VS'
/usr/bin/msbuild /verbosity:minimal /p:Configuration=Release VS/FStar.sln
Microsoft (R) Build Engine version 15.6.0.0 ( Fri Apr  6 15:55:10 UTC 2018) for Mono
Copyright (C) Microsoft Corporation. All rights reserved.

/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2067,5): warning MSB3245: Could not resolve this reference. Could not locate the assembly "FSharp.Core". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors. [/home/vagrant/FStar/src/basic/basic.fsproj]
/home/vagrant/FStar/src/basic/boot/NotFStar.Util.fs(50,5): warning FS3190: Lowercase literal 'max_int' is being shadowed by a new pattern with the same name. Only uppercase and module-prefixed literals can be used as named patterns. [/home/vagrant/FStar/src/basic/basic.fsproj]
  basic -> /home/vagrant/FStar/bin/basic.dll
  Restoring NuGet packages...
  To prevent NuGet from downloading packages during build, open the Visual Studio Options dialog, click on the Package Manager node and uncheck 'Allow NuGet to download missing packages'.
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2067,5): warning MSB3245: Could not resolve this reference. Could not locate the assembly "FSharp.Core". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors. [/home/vagrant/FStar/src/prettyprint/prettyprint.fsproj]
  prettyprint -> /home/vagrant/FStar/bin/prettyprint.dll
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2067,5): warning MSB3245: Could not resolve this reference. Could not locate the assembly "FSharp.Core". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors. [/home/vagrant/FStar/src/parser/parser.fsproj]
  compiling to dfas (can take a while...)
  367 states
  writing output
  building tables
  computing first function...time: 00:00:00.5122080
  building kernels...time: 00:00:00.7098012
  building kernel table...time: 00:00:00.0347454
  computing lookahead relations..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................time: 00:00:04.9432635
  building lookahead table...time: 00:00:02.1460913
  building action table...state 469: shift/reduce error on SEMICOLON
  state 469: shift/reduce error on SEMICOLON_SEMICOLON
  state 508: shift/reduce error on BAR
  state 512: shift/reduce error on BAR
  state 531: shift/reduce error on BAR
  state 615: shift/reduce error on COLON_EQUALS
  state 647: shift/reduce error on COLON_EQUALS
  time: 00:00:07.7657186
  building goto table...time: 00:00:02.5531448
  returning tables.
  7 shift/reduce conflicts
  891 states
  156 nonterminals
  150 terminals
  471 productions
  #rows in action table: 891
  parser -> /home/vagrant/FStar/bin/parser.dll
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2067,5): warning MSB3245: Could not resolve this reference. Could not locate the assembly "FSharp.Core". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors. [/home/vagrant/FStar/src/syntax/syntax.fsproj]
  syntax -> /home/vagrant/FStar/bin/syntax.dll
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2067,5): warning MSB3245: Could not resolve this reference. Could not locate the assembly "FSharp.Core". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors. [/home/vagrant/FStar/src/tosyntax/tosyntax.fsproj]
  tosyntax -> /home/vagrant/FStar/bin/tosyntax.dll
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2067,5): warning MSB3245: Could not resolve this reference. Could not locate the assembly "FSharp.Core". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors. [/home/vagrant/FStar/src/typechecker/typechecker.fsproj]
/home/vagrant/FStar/src/typechecker/FStar.TypeChecker.Tc.fs(1053,15): warning FS0025: Incomplete pattern matches on this expression. [/home/vagrant/FStar/src/typechecker/typechecker.fsproj]
  typechecker -> /home/vagrant/FStar/bin/typechecker.dll
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2067,5): warning MSB3245: Could not resolve this reference. Could not locate the assembly "FSharp.Core". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors. [/home/vagrant/FStar/src/format/format.fsproj]
  format -> /home/vagrant/FStar/bin/format.dll
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2067,5): warning MSB3245: Could not resolve this reference. Could not locate the assembly "FSharp.Core". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors. [/home/vagrant/FStar/src/reflection/reflection.fsproj]
  reflection -> /home/vagrant/FStar/bin/reflection.dll
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2067,5): warning MSB3245: Could not resolve this reference. Could not locate the assembly "FSharp.Core". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors. [/home/vagrant/FStar/src/extraction/extraction.fsproj]
  extraction -> /home/vagrant/FStar/bin/extraction.dll
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2067,5): warning MSB3245: Could not resolve this reference. Could not locate the assembly "FSharp.Core". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors. [/home/vagrant/FStar/src/fsdoc/fsdoc.fsproj]
  fsdoc -> /home/vagrant/FStar/bin/fsdoc.dll
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2067,5): warning MSB3245: Could not resolve this reference. Could not locate the assembly "FSharp.Core". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors. [/home/vagrant/FStar/src/smtencoding/smtencoding.fsproj]
  smtencoding -> /home/vagrant/FStar/bin/smtencoding.dll
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2067,5): warning MSB3245: Could not resolve this reference. Could not locate the assembly "FSharp.Core". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors. [/home/vagrant/FStar/src/tactics/tactics.fsproj]
  tactics -> /home/vagrant/FStar/bin/tactics.dll
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2067,5): warning MSB3245: Could not resolve this reference. Could not locate the assembly "FSharp.Core". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors. [/home/vagrant/FStar/src/fstar/fstar.fsproj]
  fstar -> /home/vagrant/FStar/bin/fstar.exe
/usr/lib/mono/msbuild/15.0/bin/Microsoft.Common.CurrentVersion.targets(2067,5): warning MSB3245: Could not resolve this reference. Could not locate the assembly "FSharp.Core". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors. [/home/vagrant/FStar/src/tests/tests.fsproj]
  tests -> /home/vagrant/FStar/bin/tests.exe
true parser/parse.fsi
chmod a+x ../bin/tests.exe
chmod a+x ../bin/fstar.exe
make: Leaving directory '/home/vagrant/FStar/src'

…and then F* isn't usable:

vagrant@ubuntu-xenial:~/FStar$ bin/fstar.exe --version
Can't find custom attr constructor image: /home/vagrant/FStar/bin/fstar.exe mtoken: 0x0a000001 due to: Could not load file or assembly 'FSharp.Core, Version=4.4.1.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' or one of its dependencies. assembly:FSharp.Core, Version=4.4.1.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a type:<unknown type> member:(null) signature:<none>

Unhandled Exception:
System.BadImageFormatException: Could not resolve field token 0x04000001, due to: Could not load type of field '<StartupCode$fstar>.$FStar.Top:format@1' (1) due to: Could not load file or assembly 'FSharp.Core, Version=4.4.1.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' or one of its dependencies. assembly:FSharp.Core, Version=4.4.1.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a type:<unknown type> member:(null) signature:<none> assembly:/home/vagrant/FStar/bin/fstar.exe type:Top member:(null) signature:<none>
File name: 'fstar'
[ERROR] FATAL UNHANDLED EXCEPTION: System.BadImageFormatException: Could not resolve field token 0x04000001, due to: Could not load type of field '<StartupCode$fstar>.$FStar.Top:format@1' (1) due to: Could not load file or assembly 'FSharp.Core, Version=4.4.1.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a' or one of its dependencies. assembly:FSharp.Core, Version=4.4.1.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a type:<unknown type> member:(null) signature:<none> assembly:/home/vagrant/FStar/bin/fstar.exe type:Top member:(null) signature:<none>
File name: 'fstar'

Here's some more version info in that VM

vagrant@ubuntu-xenial:~/FStar$ fsharpc
Microsoft (R) F# Compiler version 4.1

vagrant@ubuntu-xenial:~/FStar$ msbuild
Microsoft (R) Build Engine version 15.6.0.0 ( Fri Apr  6 15:55:10 UTC 2018) for Mono

@catalin-hritcu
Copy link
Member

catalin-hritcu commented Apr 30, 2018

@cpitclaudel Still can't reproduce, but this seems similar to point "2. Target F# Core version" of @ranweiler's original report above. Could you try to see if a similar workaround helps for you too?

Also @A-Manning's comment from a couple of weeks ago seems in that direction:
#1358 (comment)

@cpitclaudel
Copy link
Contributor

Same warnings and issue after changing to 4.3.4. Which makes sense, because the package doesn't exist on disk either:

vagrant@ubuntu-xenial:/vagrant$ ls -1 FStar/src/VS/packages/
FSharp.Compatibility.OCaml.0.1.10
FsLexYacc.6.1.0
FsLexYacc.Runtime.6.1.0
PPrintForFSharp.0.0.2

I do have some version of FSharp in system folders, though:

vagrant@ubuntu-xenial:/vagrant/FStar$ locate FSharp.Core.
/usr/lib/mono/4.5/FSharp.Core.dll
/usr/lib/mono/4.5/FSharp.Core.optdata
/usr/lib/mono/4.5/FSharp.Core.sigdata
/usr/lib/mono/fsharp/FSharp.Core.dll
/usr/lib/mono/fsharp/FSharp.Core.optdata
/usr/lib/mono/fsharp/FSharp.Core.sigdata
/usr/lib/mono/fsharp/api/.NETCore/3.259.41.0/FSharp.Core.dll
/usr/lib/mono/fsharp/api/.NETCore/3.259.41.0/FSharp.Core.optdata
/usr/lib/mono/fsharp/api/.NETCore/3.259.41.0/FSharp.Core.sigdata
/usr/lib/mono/fsharp/api/.NETCore/3.259.41.0/FSharp.Core.xml
/usr/lib/mono/fsharp/api/.NETCore/3.7.41.0/FSharp.Core.dll
/usr/lib/mono/fsharp/api/.NETCore/3.7.41.0/FSharp.Core.optdata
/usr/lib/mono/fsharp/api/.NETCore/3.7.41.0/FSharp.Core.sigdata
/usr/lib/mono/fsharp/api/.NETCore/3.7.41.0/FSharp.Core.xml
/usr/lib/mono/fsharp/api/.NETCore/3.78.41.0/FSharp.Core.dll
/usr/lib/mono/fsharp/api/.NETCore/3.78.41.0/FSharp.Core.optdata
/usr/lib/mono/fsharp/api/.NETCore/3.78.41.0/FSharp.Core.sigdata
/usr/lib/mono/fsharp/api/.NETCore/3.78.41.0/FSharp.Core.xml
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.3.0.0/FSharp.Core.dll
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.3.0.0/FSharp.Core.optdata
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.3.0.0/FSharp.Core.sigdata
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.3.0.0/FSharp.Core.xml
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.3.1.0/FSharp.Core.dll
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.3.1.0/FSharp.Core.optdata
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.3.1.0/FSharp.Core.sigdata
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.3.1.0/FSharp.Core.xml
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.4.0.0/FSharp.Core.dll
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.4.0.0/FSharp.Core.optdata
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.4.0.0/FSharp.Core.sigdata
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.4.0.0/FSharp.Core.xml
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.4.1.0/FSharp.Core.dll
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.4.1.0/FSharp.Core.optdata
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.4.1.0/FSharp.Core.sigdata
/usr/lib/mono/fsharp/api/.NETFramework/v4.0/4.4.1.0/FSharp.Core.xml
/usr/lib/mono/fsharp/api/.NETPortable/3.47.41.0/FSharp.Core.dll
/usr/lib/mono/fsharp/api/.NETPortable/3.47.41.0/FSharp.Core.optdata
/usr/lib/mono/fsharp/api/.NETPortable/3.47.41.0/FSharp.Core.sigdata
/usr/lib/mono/fsharp/api/.NETPortable/3.47.41.0/FSharp.Core.xml

@A-Manning
Copy link
Contributor

FSharp.Core 4.3.4 is the nuget package that contains FSharp.Core 4.4.3.0. My /usr/lib/mono looks the same as yours, also Ubuntu 16.04.

I can't reproduce this. You can try removing <TargetFSharpCoreVersion>4.4.3.0</TargetFSharpCoreVersion> from all of the .fsproj files. Not sure if that will help, but it's worth a try

@cpitclaudel
Copy link
Contributor

I can't reproduce this

Do you mean that you can't reproduce this on your own machine, or in a clean VM?

@cpitclaudel
Copy link
Contributor

FSharp.Core 4.3.4 is the nuget package that contains FSharp.Core 4.4.3.0.

Should I install that, then? Our installation instructions and our nuget configuration don't say cause FSharp.Core to be installed from nuget, AFAICT.

@A-Manning
Copy link
Contributor

@kant2002
Copy link
Contributor

kant2002 commented Apr 1, 2022

@nikswamy does that issue should be closed, as building F* from F# source is no longer supported?

@nikswamy
Copy link
Collaborator

nikswamy commented Apr 1, 2022

thanks. This is no longer supported. cf #2512

@nikswamy nikswamy closed this as completed Apr 1, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

6 participants