leanpkg new my_project fails

Stream: general

[Daniel Donnelly]

Using:

C:\Users\FruitfulApproach\Desktop\BlocksAndArrows\lean\bin\leanpkg new my_project
failed to start child process

manually at the comand line.

[Daniel Donnelly]

I have to get this to work manually, not with VSCode, because I'm making an IDE for lean.

[Marc Huisinga]

does it work with git bash?

[Daniel Donnelly]

@Marc Huisinga yes that works:
FruitfulApproach@DESKTOP-T49RGUJ MINGW64 ~/Desktop/BlocksAndArrows
$ lean/bin/leanpkg new my_project

mkdir -p my_project
cd my_project
mkdir src
git init -q
git checkout -b lean-3.4.2
Switched to a new branch 'lean-3.4.2'
configuring my_project 0.1

It did not work though when calling using subprocess.check_output() from code. Seems to have the same issue as non-bash command prompt.

[Daniel Donnelly]

Found this: https://stackoverflow.com/questions/4256107/running-bash-commands-in-python

Will read through it and try some things out with code.

[Andrew Ashworth]

Hmm, I remember having an issue with subprocesses on Windows. I thought it was fixed by https://github.com/leanprover/lean/commit/34426341813082e0953d323836d8ea193b3f7ffb. Might be a place to start reading if you get stuck; I do not know if this is the same problem you are having without taking a closer look.

[Daniel Donnelly]

@Andrew Ashworth I can't apply any of that code to my problem - it's in a different language from python.

[Andrew Ashworth]

You said you need to get this to work manually, though. Lean is written in C++

[Andrew Ashworth]

This is some problem with operating system process spawning, so somewhere in there is the solution, maybe?

[Daniel Donnelly]

This is some problem with operating system process spawning, so somewhere in there is the solution, maybe?

There could be a solution in there, but so far just trying different ways of calling subprocess methods (python library) has brought success. For example getting standard output from lean was crashing the process, but I just changed that to use the .communicate() method and it worked. So I will try some more things out before I check out that C++ code. Thanks though! :D

[Daniel Donnelly]

You said you need to get this to work manually, though. Lean is written in C++

It's nice to know that Lean is written in speedy C++, the fastest higher-level language really.

[Daniel Donnelly]

You said you need to get this to work manually, though. Lean is written in C++

It's nice to know that Lean is written in speedy C++, the fastest higher-level language really.

Other than Nim, Rust and a few others of course!

OTOH, when doing a GUI, python is best since there's a pyqt5 binding in existence. I have been doing pyqt5 apps for over 5 years, and it works great. When there is a computational part such as computing LED glow effect in one of my apps, I wrote a DLL in C++ that my app connects to using the ctypes library. It's similar here except we're communicating over stdin/stdout instead of by DLL.

By the way C++ was over 100 times faster at rendering a single LED than the python code, lol.

[Daniel Donnelly]

Which brings me to the question: Why don't they write Lean in D?

[Sebastian Ullrich]

I'm fairly sure someone diagnosed the "failed to start child process" error to leanpkg not finding required executables like git (which are available in a Git Bash, of course)

[Daniel Donnelly]

I'm fairly sure someone diagnosed the "failed to start child process" error to leanpkg not finding required executables like git (which are available in a Git Bash, of course)

Does that imply that the user of my IDE needs git installed first?

[Sebastian Ullrich]

Basically, yes. And even then the PATH outside of a Git Bash might not be correct, apparently

[Daniel Donnelly]

Basically, yes. And even then the PATH outside of a Git Bash might not be correct, apparently

git is present on my regular windows command prompt, when I type where git etc. So maybe I should see how I can package this with and call the git bash.

[Simon Cruanes]

Which brings me to the question: Why don't they write Lean in D?

I imagine it's because the core developers are C++ veterans, and when Lean was started, D wasn't in gcc yet, its future wasn't that walter bright.

[Sebastian Ullrich]

git is present on my regular windows command prompt, when I type where git etc.

Interesting. It might be missing some other executable. I don't remember all the ones leanpkg depends on.

[Daniel Donnelly]

It's okay, I've already thought it out: Either I provide a link in installer to install Git-for-[insert OS / or do nothing for linux], I then do a subprocess call:
git-bash and beforehand ensure that [on windows] the Path contains git-bash dir. The hardest part will be automating the setting of Path.

[Daniel Donnelly]

Would anyone like to test my code on linux / macOS's?

[Daniel Donnelly]

Looks like I'll be doing this for windows users:
https://stackoverflow.com/questions/27901880/how-to-use-python-script-to-automate-software-installation/27923165

[Daniel Donnelly]

pasted image