search

sifive / Kami

Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT
Apache License 2.0
197 stars 11 forks source link

Make command fails with Coq 8.12.1 #134

Open vaishnavi08 opened 3 years ago

vaishnavi08 commented 3 years ago

Make fails when run with Coq 8.12.1. The output is as follows: $make

coq_makefile -f _CoqProject ./All.v ./SignatureMatch.v ./Compiler/CompilerSimpleProps.v ./Compiler/CompilerProps.v ./Compiler/CompilerDoubleWrites.v ./Compiler/Compiler.v ./Compiler/Test.v ./Compiler/CompilerSimpleSem.v ./Compiler/Rtl.v ./Compiler/UnverifiedIncompleteCompiler.v ./Compiler/CompilerSimple.v ./StateMonad.v ./Tutorial/SyntaxEx.v ./Tutorial/PhoasEx.v ./Tutorial/TacticsEx.v ./Tutorial/ExtractEx.v ./Tutorial/GallinaActionEx.v ./WfActionT.v ./LibStruct.v ./PProperties.v ./WfMod_Helper.v ./Passes.v ./AllNotations.v ./NotationsTest.v ./Rewrites/ReflectionPre.v ./Rewrites/ReflectionSoundTheorems1.v ./Rewrites/ReflectionOrig.v ./Rewrites/ReflectionSoundTopTheorems.v ./Rewrites/Notations_rewrites.v ./Rewrites/ReflectionImpl.v ./Rewrites/ReflectionSoundTheorems2.v ./PPlusProperties.v ./GallinaModules/Relations.v ./GallinaModules/AuxLemmas.v ./GallinaModules/AuxTactics.v ./Lib/HexNotation.v ./Lib/NatStr.v ./Lib/EclecticLib.v ./Lib/WordProperties.v ./Lib/HexNotationWord.v ./Lib/Word.v ./Lib/VectorFacts.v ./Lib/Fold.v ./Extraction.v ./AllDefn.v ./Guard.v ./Tactics.v ./Properties.v ./Utila.v ./Syntax.v ./Notations.v ./Simulator/NativeTest.v ./Simulator/CoqSim/Misc.v ./Simulator/CoqSim/Eval.v ./Simulator/CoqSim/TransparentProofs.v ./Simulator/CoqSim/RegisterFile.v ./Simulator/CoqSim/Simulator.v ./Simulator/CoqSim/HaskellTypes.v ./SyntaxDoubleWrites.v -o Makefile.coq.all
Warning: no common logical root
Warning: in such case INSTALLDEFAULTROOT must be defined
Warning: the install-doc target is going to install files
Warning: in orphan_Kami_RecordUpdate
make -f Makefile.coq.all
make[1]: Entering directory '/home/vaishnavi/Kami'
COQDEP VFILES
Fatal error: exception Sys_error("../coq-record-update/src: No such file or directory")
COQDEP VFILES
Fatal error: exception Sys_error("../coq-record-update/src: No such file or directory")
COQDEP VFILES
Fatal error: exception Sys_error("../coq-record-update/src: No such file or directory")
COQC All.v
While loading initial state:
Warning: Cannot open ../coq-record-update/src [cannot-open-path,filesystem]
File "./All.v", line 1, characters 15-32:
Error: Unable to locate library Kami.AllNotations.

Makefile.coq.all:658: recipe for target 'All.vo' failed
make[2]: *** [All.vo] Error 1
Makefile.coq.all:320: recipe for target 'all' failed
make[1]: *** [all] Error 2
make[1]: Leaving directory '/home/vaishnavi/Kami'
Makefile:6: recipe for target 'coq' failed
make: *** [coq] Error 2
nanoeng commented 3 years ago

I came across the same problem. My setup uses Coq proof assistant v8.11.0 and OCaml v4.08.1 and runs on a WSL Ubuntu 20.04

JasonGross commented 3 years ago

I believe this repo assumes that it's dependencies live in the same parent folder. So you need to clone coq-record-update and any other dependencies. See https://github.com/mit-plv/bedrock2/tree/master/deps for an example of this in action.

kendroe commented 3 years ago

I thought I'd put out a note that Intel is looking for formal verification engineers. Anyone who is looking at this repository is likely qualified for a good paying job. You can send a message to my LinkedIn profile at https://www.linkedin.com/in/kenneth-roe-7ba4303/ and I'll make sure the resume gets to the right person.

             - Ken

[https://media-exp1.licdn.com/dms/image/C4E03AQFphIQArC-G8A/profile-displayphoto-shrink_200_200/0/1516303657460?e=1642032000&v=beta&t=to7EGGjHdeXoNJIh6EaNtPv9bSAHYLNUDNfb7yeFXwk]https://www.linkedin.com/in/kenneth-roe-7ba4303/ Kenneth Roe – Wien, Wien, Österreich | Berufsprofil | LinkedInhttps://www.linkedin.com/in/kenneth-roe-7ba4303/ Sehen Sie sich das Profil von Kenneth Roe auf LinkedIn an. Als weltweit größtes Business-Netzwerk hilft LinkedIn Menschen wie Kenneth Roe dabei, Kontakte zu finden, die mit empfohlenen Kandidaten, Branchenexperten und potenziellen Geschäftspartnern vernetzt sind. www.linkedin.com

          - Ken

From: Jason Gross @.> Sent: Tuesday, November 9, 2021 3:23 PM To: sifive/Kami @.> Cc: Subscribed @.***> Subject: Re: [sifive/Kami] Make command fails with Coq 8.12.1 (#134)

I believe this repo assumes that it's dependencies live in the same parent folder. So you need to clone coq-record-update and any other dependencies. See https://github.com/mit-plv/bedrock2/tree/master/depshttps://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fmit-plv%2Fbedrock2%2Ftree%2Fmaster%2Fdeps&data=04%7C01%7C%7Cd53b361d88074446c6cc08d9a38c87b7%7C84df9e7fe9f640afb435aaaaaaaaaaaa%7C1%7C0%7C637720646239271165%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=HegHXetZhO%2BekKPtRu5jGS29vn390eti04D1%2B88%2BeUs%3D&reserved=0 for an example of this in action.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fsifive%2FKami%2Fissues%2F134%23issuecomment-964197996&data=04%7C01%7C%7Cd53b361d88074446c6cc08d9a38c87b7%7C84df9e7fe9f640afb435aaaaaaaaaaaa%7C1%7C0%7C637720646239281121%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=XwtCV1jAtrluUUUnqyjgm%2BDVr%2BPExGusfCP33KErLiY%3D&reserved=0, or unsubscribehttps://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAB2KXSCDYU2JUBEUGPUISD3ULEVGZANCNFSM5D7YWJYA&data=04%7C01%7C%7Cd53b361d88074446c6cc08d9a38c87b7%7C84df9e7fe9f640afb435aaaaaaaaaaaa%7C1%7C0%7C637720646239291076%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=nIdlxqX4My2oK9XyVvF1t8hvB7QM2bh1xuVsii7SGaY%3D&reserved=0. Triage notifications on the go with GitHub Mobile for iOShttps://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fapps.apple.com%2Fapp%2Fapple-store%2Fid1477376905%3Fct%3Dnotification-email%26mt%3D8%26pt%3D524675&data=04%7C01%7C%7Cd53b361d88074446c6cc08d9a38c87b7%7C84df9e7fe9f640afb435aaaaaaaaaaaa%7C1%7C0%7C637720646239301032%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=2jg6mqL99717zraSJNWWUchFSXiGTIDKNAwBzfwO1U4%3D&reserved=0 or Androidhttps://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fplay.google.com%2Fstore%2Fapps%2Fdetails%3Fid%3Dcom.github.android%26referrer%3Dutm_campaign%253Dnotification-email%2526utm_medium%253Demail%2526utm_source%253Dgithub&data=04%7C01%7C%7Cd53b361d88074446c6cc08d9a38c87b7%7C84df9e7fe9f640afb435aaaaaaaaaaaa%7C1%7C0%7C637720646239301032%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=c4G8Ft%2FPNpoQxHJM69ZiHef6jLa9w98kPP1Zl36RiZY%3D&reserved=0.