Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari

mukeshtiwari/gist:dfbff8e4573c40aea9b5f646184315d3

Created January 14, 2024 10:21
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save mukeshtiwari/dfbff8e4573c40aea9b5f646184315d3 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save mukeshtiwari/dfbff8e4573c40aea9b5f646184315d3 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
mukeshtiwari@Mukeshs-MacBook-Pro exercises % make
coq_makefile -f _CoqProject -o Makefile.coq
/Library/Developer/CommandLineTools/usr/bin/make -f Makefile.coq
COQDEP VFILES
*** Warning: in file MetaCoqPrelude.v, library All is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file MetaCoqPrelude.v, library Checker is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file MetaCoqPrelude.v, library Reduction is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file ./MetaCoqPrelude.v, library All is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file ./MetaCoqPrelude.v, library Checker is required from root MetaCoq.Template and has not been found in the loadpath!
*** Warning: in file ./MetaCoqPrelude.v, library Reduction is required from root MetaCoq.Template and has not been found in the loadpath!
COQC MetaCoqPrelude.v
File "./MetaCoqPrelude.v", line 5, characters 0-59:
Error: Cannot find a physical path bound to logical path
All with prefix MetaCoq.Template.
make[2]: *** [MetaCoqPrelude.vo] Error 1
make[1]: *** [all] Error 2
make: *** [all] Error 2
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment