K framework install failure on MacOS catalina 10.15.6

76 views Asked by At

Hi I am on MacOS catalina 10.15.6 and am trying to install the K-framework using

brew reinstall kframework

I keep getting the error:

Fatal error:    OpamSystem.File_not_found("/usr/local/Cellar/kframework/5.0.0/lib/kframework/opamroot/repo/k/packages/mlgmp/mlgmp.20150824/opam")

I reinstalled ocaml and opam and that worked but the above error persists!

So I brew uninstall kframework then brew install kframework but now get the error

   [ERROR] Compiler selection '4.10.0' is ambiguous. matching packages: { ocaml-base-compiler.4.10.0, ocaml-system.4.10.0 }
    The following dependencies couldn't be met:
      - mlgmp → ocaml < 4.06.0
          base of this switch (use `--unlock-base' to force)

No solution found, exiting

Any help much appreciated? david

Today it installs with no errors or warnings:

Trying to test/use kompile but all attempts to use lesson_1/imp1.k fail with

dstr@Dstr lesson_1 % kompile imp.k
[Error] Compiler: Could not find sorts: [Id]
    Source(/Users/dstr/K/tutorial/1_k/4_imp++/lesson_1/./imp.k)
    Location(17,20,17,57)
dstr@Dstr lesson_1 % kompile --debug imp.k
org.kframework.utils.errorsystem.KEMException: [Error] Compiler: Could not find sorts: [Id]
    Source(/Users/dstr/K/tutorial/1_k/4_imp++/lesson_1/./imp.k)
    Location(17,20,17,57)

Is this because imp.k is out of date or is there something still wrong with my install? (if imp.k is out of date where can I get some upto date _.k files?)

No problems found the recent files all is working. Many thanks.

0

There are 0 answers