search

DanGrayson / Foundations2

Development of the univalent foundations of mathematics in Coq
http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html
0 stars 0 forks source link

"type" command #1

Open benediktahrens opened 10 years ago

benediktahrens commented 10 years ago

Compiling branch for-coq-8.4 I get

0.09 sec, 18264 bytes: Proof_of_Extensionality/funextfun type coqc make: type: Command not found make: *\ [announce] Error 127 ahrens@alien:~/git/benediktahrens/Foundations$

Because of the name of the command, I am having some trouble finding out whether I am missing a package or what else to do...

DanGrayson commented 10 years ago

Oh, just kill that line in the makefile -- it's supposed to display the location of coqc so I can see whether I'm using the right makefile.

But it's a feature of bash, a built-in command, so why don't you have it? Have you set SHELL to something else?

On Thu, Jan 23, 2014 at 5:38 AM, benediktahrens notifications@github.comwrote:

Compiling branch for-coq-8.4 I get

0.09 sec, 18264 bytes: Proof_of_Extensionality/funextfun type coqc make: type: Command not found make: *\ [announce] Error 127 ahrens@alien:~/git/benediktahrens/Foundations$

Because of the name of the command, I am having some trouble finding out whether I am missing a package or what else to do...

— Reply to this email directly or view it on GitHubhttps://github.com/DanGrayson/Foundations2/issues/1 .

benediktahrens commented 10 years ago

Actually, $ type coqc works from the cmdline, but not from within the Makefile, I don't know why. Replacing type by which in the Makefile works for me.

On 01/23/2014 02:58 PM, Daniel R. Grayson wrote:

Oh, just kill that line in the makefile -- it's supposed to display the location of coqc so I can see whether I'm using the right makefile.

But it's a feature of bash, a built-in command, so why don't you have it? Have you set SHELL to something else?

On Thu, Jan 23, 2014 at 5:38 AM, benediktahrens notifications@github.comwrote:

Compiling branch for-coq-8.4 I get

0.09 sec, 18264 bytes: Proof_of_Extensionality/funextfun type coqc make: type: Command not found make: *\ [announce] Error 127 ahrens@alien:~/git/benediktahrens/Foundations$

Because of the name of the command, I am having some trouble finding out whether I am missing a package or what else to do...

— Reply to this email directly or view it on GitHubhttps://github.com/DanGrayson/Foundations2/issues/1 .

Reply to this email directly or view it on GitHub: https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33125457

DanGrayson commented 10 years ago

Probably because /bin/sh is dash instead of bash on your machine. Try running the type command after starting "sh".

On Thu, Jan 23, 2014 at 9:03 AM, benediktahrens notifications@github.comwrote:

Actually, $ type coqc works from the cmdline, but not from within the Makefile, I don't know why. Replacing type by which in the Makefile works for me.

On 01/23/2014 02:58 PM, Daniel R. Grayson wrote:

Oh, just kill that line in the makefile -- it's supposed to display the location of coqc so I can see whether I'm using the right makefile.

But it's a feature of bash, a built-in command, so why don't you have it? Have you set SHELL to something else?

On Thu, Jan 23, 2014 at 5:38 AM, benediktahrens < notifications@github.com>wrote:

Compiling branch for-coq-8.4 I get

0.09 sec, 18264 bytes: Proof_of_Extensionality/funextfun type coqc make: type: Command not found make: *\ [announce] Error 127 ahrens@alien:~/git/benediktahrens/Foundations$

Because of the name of the command, I am having some trouble finding out whether I am missing a package or what else to do...

— Reply to this email directly or view it on GitHub< https://github.com/DanGrayson/Foundations2/issues/1> .

Reply to this email directly or view it on GitHub:

https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33125457

— Reply to this email directly or view it on GitHubhttps://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33125799 .

benediktahrens commented 10 years ago

/bin/sh is indeed dash on my machine, but dash knows type. It is only in the Makefile that the call does not work.

On 01/23/2014 03:28 PM, Daniel R. Grayson wrote:

Probably because /bin/sh is dash instead of bash on your machine. Try running the type command after starting "sh".

On Thu, Jan 23, 2014 at 9:03 AM, benediktahrens notifications@github.comwrote:

Actually, $ type coqc works from the cmdline, but not from within the Makefile, I don't know why. Replacing type by which in the Makefile works for me.

On 01/23/2014 02:58 PM, Daniel R. Grayson wrote:

Oh, just kill that line in the makefile -- it's supposed to display the location of coqc so I can see whether I'm using the right makefile.

But it's a feature of bash, a built-in command, so why don't you have it? Have you set SHELL to something else?

On Thu, Jan 23, 2014 at 5:38 AM, benediktahrens < notifications@github.com>wrote:

Compiling branch for-coq-8.4 I get

0.09 sec, 18264 bytes: Proof_of_Extensionality/funextfun type coqc make: type: Command not found make: *\ [announce] Error 127 ahrens@alien:~/git/benediktahrens/Foundations$

Because of the name of the command, I am having some trouble finding out whether I am missing a package or what else to do...

— Reply to this email directly or view it on GitHub< https://github.com/DanGrayson/Foundations2/issues/1> .

Reply to this email directly or view it on GitHub:

https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33125457

— Reply to this email directly or view it on GitHubhttps://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33125799 .

Reply to this email directly or view it on GitHub: https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33127766

DanGrayson commented 10 years ago

I figured out why. On your machine, "make" looks at "type coqc" and discerns that the command uses no features of the shell (such as > or |) and can be run directly. So it tries to execute the program "type", but doesn't find it, because it's a shell built-in. If the command had been "type coqc | cat" it would have worked.

On my machine, /usr/bin/type exists and is found, in that circumstance.

On Thu, Jan 23, 2014 at 11:00 AM, benediktahrens notifications@github.comwrote:

/bin/sh is indeed dash on my machine, but dash knows type. It is only in the Makefile that the call does not work.

On 01/23/2014 03:28 PM, Daniel R. Grayson wrote:

Probably because /bin/sh is dash instead of bash on your machine. Try running the type command after starting "sh".

On Thu, Jan 23, 2014 at 9:03 AM, benediktahrens < notifications@github.com>wrote:

Actually, $ type coqc works from the cmdline, but not from within the Makefile, I don't know why. Replacing type by which in the Makefile works for me.

On 01/23/2014 02:58 PM, Daniel R. Grayson wrote:

Oh, just kill that line in the makefile -- it's supposed to display the location of coqc so I can see whether I'm using the right makefile.

But it's a feature of bash, a built-in command, so why don't you have it? Have you set SHELL to something else?

On Thu, Jan 23, 2014 at 5:38 AM, benediktahrens < notifications@github.com>wrote:

Compiling branch for-coq-8.4 I get

0.09 sec, 18264 bytes: Proof_of_Extensionality/funextfun type coqc make: type: Command not found make: *\ [announce] Error 127 ahrens@alien:~/git/benediktahrens/Foundations$

Because of the name of the command, I am having some trouble finding out whether I am missing a package or what else to do...

— Reply to this email directly or view it on GitHub< https://github.com/DanGrayson/Foundations2/issues/1> .

Reply to this email directly or view it on GitHub:

https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33125457

— Reply to this email directly or view it on GitHub< https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33125799> .

Reply to this email directly or view it on GitHub:

https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33127766

— Reply to this email directly or view it on GitHubhttps://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33137201 .

benediktahrens commented 10 years ago

Oh, ok. Is which installed on MacOS? Could I just stick with that?

On 01/23/2014 05:47 PM, Daniel R. Grayson wrote:

I figured out why. On your machine, "make" looks at "type coqc" and discerns that the command uses no features of the shell (such as > or |) and can be run directly. So it tries to execute the program "type", but doesn't find it, because it's a shell built-in. If the command had been "type coqc | cat" it would have worked.

On my machine, /usr/bin/type exists and is found, in that circumstance.

On Thu, Jan 23, 2014 at 11:00 AM, benediktahrens notifications@github.comwrote:

/bin/sh is indeed dash on my machine, but dash knows type. It is only in the Makefile that the call does not work.

On 01/23/2014 03:28 PM, Daniel R. Grayson wrote:

Probably because /bin/sh is dash instead of bash on your machine. Try running the type command after starting "sh".

On Thu, Jan 23, 2014 at 9:03 AM, benediktahrens < notifications@github.com>wrote:

Actually, $ type coqc works from the cmdline, but not from within the Makefile, I don't know why. Replacing type by which in the Makefile works for me.

On 01/23/2014 02:58 PM, Daniel R. Grayson wrote:

Oh, just kill that line in the makefile -- it's supposed to display the location of coqc so I can see whether I'm using the right makefile.

But it's a feature of bash, a built-in command, so why don't you have it? Have you set SHELL to something else?

On Thu, Jan 23, 2014 at 5:38 AM, benediktahrens < notifications@github.com>wrote:

Compiling branch for-coq-8.4 I get

0.09 sec, 18264 bytes: Proof_of_Extensionality/funextfun type coqc make: type: Command not found make: *\ [announce] Error 127 ahrens@alien:~/git/benediktahrens/Foundations$

Because of the name of the command, I am having some trouble finding out whether I am missing a package or what else to do...

— Reply to this email directly or view it on GitHub< https://github.com/DanGrayson/Foundations2/issues/1> .

Reply to this email directly or view it on GitHub:

https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33125457

— Reply to this email directly or view it on GitHub< https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33125799> .

Reply to this email directly or view it on GitHub:

https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33127766

— Reply to this email directly or view it on GitHubhttps://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33137201 .

Reply to this email directly or view it on GitHub: https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33142553

DanGrayson commented 10 years ago

Yes, stick with "which".

On Thu, Jan 23, 2014 at 12:40 PM, benediktahrens notifications@github.comwrote:

Oh, ok. Is which installed on MacOS? Could I just stick with that?

On 01/23/2014 05:47 PM, Daniel R. Grayson wrote:

I figured out why. On your machine, "make" looks at "type coqc" and discerns that the command uses no features of the shell (such as > or |) and can be run directly. So it tries to execute the program "type", but doesn't find it, because it's a shell built-in. If the command had been "type coqc | cat" it would have worked.

On my machine, /usr/bin/type exists and is found, in that circumstance.

On Thu, Jan 23, 2014 at 11:00 AM, benediktahrens notifications@github.comwrote:

/bin/sh is indeed dash on my machine, but dash knows type. It is only in the Makefile that the call does not work.

On 01/23/2014 03:28 PM, Daniel R. Grayson wrote:

Probably because /bin/sh is dash instead of bash on your machine. Try running the type command after starting "sh".

On Thu, Jan 23, 2014 at 9:03 AM, benediktahrens < notifications@github.com>wrote:

Actually, $ type coqc works from the cmdline, but not from within the Makefile, I don't know why. Replacing type by which in the Makefile works for me.

On 01/23/2014 02:58 PM, Daniel R. Grayson wrote:

Oh, just kill that line in the makefile -- it's supposed to display the location of coqc so I can see whether I'm using the right makefile.

But it's a feature of bash, a built-in command, so why don't you have it? Have you set SHELL to something else?

On Thu, Jan 23, 2014 at 5:38 AM, benediktahrens < notifications@github.com>wrote:

Compiling branch for-coq-8.4 I get

0.09 sec, 18264 bytes: Proof_of_Extensionality/funextfun type coqc make: type: Command not found make: *\ [announce] Error 127 ahrens@alien:~/git/benediktahrens/Foundations$

Because of the name of the command, I am having some trouble finding out whether I am missing a package or what else to do...

— Reply to this email directly or view it on GitHub< https://github.com/DanGrayson/Foundations2/issues/1> .

Reply to this email directly or view it on GitHub:

https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33125457

— Reply to this email directly or view it on GitHub<

https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33125799>

.

Reply to this email directly or view it on GitHub:

https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33127766

— Reply to this email directly or view it on GitHub< https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33137201> .

Reply to this email directly or view it on GitHub:

https://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33142553

— Reply to this email directly or view it on GitHubhttps://github.com/DanGrayson/Foundations2/issues/1#issuecomment-33148171 .