Skip to content

Minor refactor of elan-init.ps1 for ContrainedLanguage Mode - #204

Merged
Kha merged 3 commits into
leanprover:masterfrom
davide-pozzoni-uk-gt:master
Jun 19, 2026
Merged

Minor refactor of elan-init.ps1 for ContrainedLanguage Mode#204
Kha merged 3 commits into
leanprover:masterfrom
davide-pozzoni-uk-gt:master

Conversation

@davide-pozzoni-uk-gt

Copy link
Copy Markdown
Contributor

The current version of elan-init.ps1 does not work in ConstrainedLanguage Mode of powershell for only one line

$temp = [System.IO.Path]::GetTempPath()

Replace that line with $env equivalents to work in ConstrainedLanguage Mode

$temp = $env:TMP
if (-not $temp) { $temp = $env:TEMP }
if (-not $temp) { $temp = $env:USERPROFILE }

@Kha

Kha commented Jun 18, 2026

Copy link
Copy Markdown
Member

So what happens if none of these are set? This PR doesn't seem very thought through tbh.

@davide-pozzoni-uk-gt

davide-pozzoni-uk-gt commented Jun 18, 2026

Copy link
Copy Markdown
Contributor Author

So what happens if none of these are set? This PR doesn't seem very thought through tbh.

the fallback of GetTempPath() when it cannot retreive TMP or TEMP or USERPROFILE, is $env:SystemRoot } # e.g. C:\Windows

I can add if (-not $temp) { $temp = $env:SystemRoot } too if you prefer (even tho it is extremely unlikely that it would fallback to that)

GetTempPath() is a lookup function (with lookup order TMP → TEMP → USERPROFILE → Windows dir)
image
https://learn.microsoft.com/en-us/windows/win32/api/fileapi/nf-fileapi-gettemppathw

Refactor temporary directory resolution for ConstrainedLanguage mode.
@davide-pozzoni-uk-gt

davide-pozzoni-uk-gt commented Jun 18, 2026

Copy link
Copy Markdown
Contributor Author

0fb33b8
now the only difference between the $env behaviour and [System.IO.Path]::GetTempPath() is that the latter is cross-platform compatible https://learn.microsoft.com/en-us/dotnet/api/system.io.path.gettemppath?view=net-10.0&tabs=linux. But this script only supports windows anyway, so I believe that is not relevant. That said for cross-platform compatibility

if ($IsLinux -or $IsMacOS) {
    $temp = $env:TMPDIR
    if (-not $temp) { $temp = '/tmp' }
}
else {
    $temp = $env:TMP
    if (-not $temp) { $temp = $env:TEMP }
    if (-not $temp) { $temp = $env:USERPROFILE }
    if (-not $temp) { $temp = $env:SystemRoot }
}

it can use that

@Kha
Kha enabled auto-merge (squash) June 19, 2026 08:11
@Kha

Kha commented Jun 19, 2026

Copy link
Copy Markdown
Member

Thanks!

@Kha
Kha disabled auto-merge June 19, 2026 08:12
@Kha
Kha enabled auto-merge (squash) June 19, 2026 08:12
@Kha
Kha merged commit 6737edc into leanprover:master Jun 19, 2026
5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants