Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 14 additions & 4 deletions macos/internal/gui/app.go
Original file line number Diff line number Diff line change
Expand Up @@ -127,15 +127,25 @@ func runInstall(ctx *sharedgui.InstallContext, m *manifest.Manifest, templates f
ctx.LogPanel.Append(fmt.Sprintf("Installed app: %s", result.InstalledApp))
ctx.LogPanel.Append("Workspace: ~/rocq-workspace")

if result.VsrocqtopWarning != "" {
ctx.LogPanel.Append(fmt.Sprintf("WARNING: %s", result.VsrocqtopWarning))
}

if ctx.Checklist != nil {
ctx.Checklist.AppendSummary("")
ctx.Checklist.AppendSummary(fmt.Sprintf("Installation complete! (%s)", elapsed))
ctx.Checklist.AppendSummary(fmt.Sprintf("Installed app: %s", result.InstalledApp))
ctx.Checklist.AppendSummary("Workspace: ~/rocq-workspace")
if result.VsrocqtopWarning != "" {
ctx.Checklist.AppendSummary(fmt.Sprintf("WARNING: %s", result.VsrocqtopWarning))
}
}

sharedgui.ShowSuccess(ctx.Window,
fmt.Sprintf("Rocq Platform has been installed successfully in %s.\n\n", elapsed)+
fmt.Sprintf("Installed app: %s\n", result.InstalledApp)+
"Workspace: ~/rocq-workspace")
successMsg := fmt.Sprintf("Rocq Platform has been installed successfully in %s.\n\n", elapsed) +
fmt.Sprintf("Installed app: %s\n", result.InstalledApp) +
"Workspace: ~/rocq-workspace"
if result.VsrocqtopWarning != "" {
successMsg += fmt.Sprintf("\n\nWarning: %s", result.VsrocqtopWarning)
}
sharedgui.ShowSuccess(ctx.Window, successMsg)
}
11 changes: 7 additions & 4 deletions macos/internal/installer/installer.go
Original file line number Diff line number Diff line change
Expand Up @@ -124,9 +124,10 @@ func FindExistingInstallations() []string {

// Result holds information about the installation outcome.
type Result struct {
VSCodeFound bool // Whether VSCode was detected on the system
InstalledApp string // Path to the installed .app
VsrocqtopPath string // Path to vsrocqtop binary
VSCodeFound bool // Whether VSCode was detected on the system
InstalledApp string // Path to the installed .app
VsrocqtopPath string // Path to vsrocqtop binary
VsrocqtopWarning string // Non-empty if vsrocqtop was not found
}

// Run executes the installation pipeline.
Expand Down Expand Up @@ -220,7 +221,9 @@ func Run(cfg *Config) (*Result, error) {
cfg.OnStep(4, fmt.Sprintf("Locating %s...", topBinLabel), 0.0)
vsrocqtopPath, err := FindLanguageServerTop(installedAppPath, cfg.Manifest.RocqVersion)
if err != nil {
cfg.Logger.Log("WARNING: %s not found: %v", topBinLabel, err)
warnMsg := fmt.Sprintf("%s not found: %v. VSCode will not be able to check proofs until this is resolved.", topBinLabel, err)
cfg.Logger.Log("WARNING: %s", warnMsg)
result.VsrocqtopWarning = warnMsg
cfg.OnStep(4, fmt.Sprintf("%s not found (will skip VSCode settings).", topBinLabel), 1.0)
} else {
cfg.Logger.Log("Found %s: %s", topBinLabel, vsrocqtopPath)
Expand Down
8 changes: 4 additions & 4 deletions macos/internal/installer/vsrocqtop.go
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ import (

// FindLanguageServerTop searches for the vsrocqtop or vscoqtop binary depending on the version.
// Search order:
// 1. Inside the installed .app bundle (Contents/ walk, max depth 6)
// 1. Inside the installed .app bundle (Contents/ walk, max depth 10)
// 2. exec.LookPath
// 3. Known paths: /usr/local/bin, /opt/homebrew/bin
// 4. Scan /Applications and ~/Applications for *rocq*.app / *coq*.app
Expand All @@ -28,8 +28,8 @@ func FindLanguageServerTop(installedAppPath, rocqVersion string) (string, error)
if installedAppPath != "" {
contentsDir := filepath.Join(installedAppPath, "Contents")
if info, err := os.Stat(contentsDir); err == nil && info.IsDir() {
debugLog("[%s] searching in %s (max depth 6)", binName, contentsDir)
found := walkForBinary(contentsDir, binName, 6)
debugLog("[%s] searching in %s (max depth 10)", binName, contentsDir)
found := walkForBinary(contentsDir, binName, 10)
if found != "" {
debugLog("[%s] FOUND in app bundle: %s", binName, found)
return found, nil
Expand Down Expand Up @@ -77,7 +77,7 @@ func FindLanguageServerTop(installedAppPath, rocqVersion string) (string, error)
}
appContents := filepath.Join(baseDir, e.Name(), "Contents")
if info, err := os.Stat(appContents); err == nil && info.IsDir() {
found := walkForBinary(appContents, binName, 6)
found := walkForBinary(appContents, binName, 10)
if found != "" {
debugLog("[%s] FOUND in app scan: %s", binName, found)
return found, nil
Expand Down
12 changes: 6 additions & 6 deletions shared/gui/stepchecklist.go
Original file line number Diff line number Diff line change
Expand Up @@ -28,13 +28,13 @@ func NewStepChecklist(steps []string) *StepChecklist {

rows := make([]fyne.CanvasObject, 0, len(steps)*2)
for i, name := range steps {
icon := canvas.NewText(" ○ ", rocqMutedText)
icon := canvas.NewText(" ○ ", rocqLightDisabled)
icon.TextSize = 13

label := canvas.NewText(name, rocqMutedText)
label := canvas.NewText(name, rocqLightDisabled)
label.TextSize = 13

detail := canvas.NewText("", rocqMutedText)
detail := canvas.NewText("", rocqLightDisabled)
detail.TextSize = 11
detail.Hide()

Expand Down Expand Up @@ -73,7 +73,7 @@ func (sc *StepChecklist) SetInProgress(step int, detail string) {
sc.icons[idx].Text = " ▶ "
sc.icons[idx].Color = RocqOrange
sc.icons[idx].Refresh()
sc.names[idx].Color = rocqDarkText
sc.names[idx].Color = rocqLightFg
sc.names[idx].TextStyle = fyne.TextStyle{Bold: true}
sc.names[idx].Refresh()
sc.setDetail(idx, detail)
Expand Down Expand Up @@ -104,7 +104,7 @@ func (sc *StepChecklist) markDone(idx int) {
sc.icons[idx].Text = " ✓ "
sc.icons[idx].Color = rocqSuccess
sc.icons[idx].Refresh()
sc.names[idx].Color = rocqDarkText
sc.names[idx].Color = rocqLightFg
sc.names[idx].TextStyle = fyne.TextStyle{}
sc.names[idx].Refresh()
}
Expand All @@ -121,7 +121,7 @@ func (sc *StepChecklist) setDetail(idx int, text string) {

// AppendSummary adds a summary line below the checklist steps.
func (sc *StepChecklist) AppendSummary(text string) {
line := canvas.NewText(text, rocqDarkText)
line := canvas.NewText(text, rocqLightFg)
line.TextSize = 12
sc.Container.Add(line)
}
Expand Down
82 changes: 60 additions & 22 deletions shared/gui/theme.go
Original file line number Diff line number Diff line change
Expand Up @@ -10,16 +10,28 @@ import (
// Rocq brand colors from https://rocq-prover.org/ logo.
// Logo uses #260085 (deep blue) and #ff540a (bright orange).
var (
rocqLightBg = color.NRGBA{R: 0xf0, G: 0xef, B: 0xf5, A: 0xff} // light background with blue tint
rocqAccent = color.NRGBA{R: 0xff, G: 0x54, B: 0x0a, A: 0xff} // brand orange for focus (#ff540a)
rocqHover = color.NRGBA{R: 0xe8, G: 0xe6, B: 0xf0, A: 0xff} // subtle blue-tinted hover
rocqSelection = color.NRGBA{R: 0xd8, G: 0xd4, B: 0xe8, A: 0xff} // soft blue-tinted selection
rocqSeparator = color.NRGBA{R: 0xd0, G: 0xce, B: 0xda, A: 0xff} // subtle separator
rocqInputBg = color.NRGBA{R: 0xff, G: 0xff, B: 0xff, A: 0xff} // white input fields
rocqDarkText = color.NRGBA{R: 0x1a, G: 0x0a, B: 0x3a, A: 0xff} // dark text with blue undertone
rocqMutedText = color.NRGBA{R: 0x6b, G: 0x6b, B: 0x6b, A: 0xff} // muted text
rocqSuccess = color.NRGBA{R: 0x2e, G: 0x7d, B: 0x32, A: 0xff} // green for success
rocqError = color.NRGBA{R: 0xc6, G: 0x28, B: 0x28, A: 0xff} // red for errors
// Light mode colors
rocqLightBg = color.NRGBA{R: 0xf0, G: 0xef, B: 0xf5, A: 0xff} // light background with blue tint
rocqAccent = color.NRGBA{R: 0xff, G: 0x54, B: 0x0a, A: 0xff} // brand orange for focus (#ff540a)
rocqLightHover = color.NRGBA{R: 0xe8, G: 0xe6, B: 0xf0, A: 0xff} // subtle blue-tinted hover
rocqLightSelection = color.NRGBA{R: 0xd8, G: 0xd4, B: 0xe8, A: 0xff} // soft blue-tinted selection
rocqLightSeparator = color.NRGBA{R: 0xd0, G: 0xce, B: 0xda, A: 0xff} // subtle separator
rocqLightInputBg = color.NRGBA{R: 0xff, G: 0xff, B: 0xff, A: 0xff} // white input fields
rocqLightFg = color.NRGBA{R: 0x1a, G: 0x0a, B: 0x3a, A: 0xff} // dark text with blue undertone
rocqLightDisabled = color.NRGBA{R: 0x6b, G: 0x6b, B: 0x6b, A: 0xff} // muted text

// Dark mode colors
rocqDarkBg = color.NRGBA{R: 0x1e, G: 0x1b, B: 0x2e, A: 0xff} // dark background with blue tint
rocqDarkHover = color.NRGBA{R: 0x2e, G: 0x2a, B: 0x42, A: 0xff} // dark hover
rocqDarkSelection = color.NRGBA{R: 0x3a, G: 0x35, B: 0x55, A: 0xff} // dark selection
rocqDarkSeparator = color.NRGBA{R: 0x3e, G: 0x3a, B: 0x52, A: 0xff} // dark separator
rocqDarkInputBg = color.NRGBA{R: 0x2a, G: 0x27, B: 0x3e, A: 0xff} // dark input fields
rocqDarkFg = color.NRGBA{R: 0xe8, G: 0xe6, B: 0xf0, A: 0xff} // light text for dark mode
rocqDarkDisabled = color.NRGBA{R: 0x8a, G: 0x8a, B: 0x9a, A: 0xff} // lighter muted text for dark mode

// Shared brand colors (same in both modes)
rocqSuccess = color.NRGBA{R: 0x2e, G: 0x7d, B: 0x32, A: 0xff} // green for success
rocqError = color.NRGBA{R: 0xc6, G: 0x28, B: 0x28, A: 0xff} // red for errors

// RocqOrange is the brand orange (#ff540a), exported for use in GUI components.
RocqOrange = color.NRGBA{R: 0xff, G: 0x54, B: 0x0a, A: 0xff}
Expand All @@ -38,31 +50,57 @@ func NewRocqTheme() fyne.Theme {
}

func (t *rocqTheme) Color(name fyne.ThemeColorName, variant fyne.ThemeVariant) color.Color {
dark := variant == theme.VariantDark

switch name {
// Brand colors — same in both modes
case theme.ColorNamePrimary:
return RocqOrange
case theme.ColorNameButton:
return RocqOrange
case theme.ColorNameHover:
return rocqHover
case theme.ColorNameFocus:
return rocqAccent
case theme.ColorNameSelection:
return rocqSelection
case theme.ColorNameSuccess:
return rocqSuccess
case theme.ColorNameError:
return rocqError

// Variant-dependent colors
case theme.ColorNameBackground:
if dark {
return rocqDarkBg
}
return rocqLightBg
case theme.ColorNameForeground:
return rocqDarkText
if dark {
return rocqDarkFg
}
return rocqLightFg
case theme.ColorNameInputBackground:
return rocqInputBg
if dark {
return rocqDarkInputBg
}
return rocqLightInputBg
case theme.ColorNameHover:
if dark {
return rocqDarkHover
}
return rocqLightHover
case theme.ColorNameSelection:
if dark {
return rocqDarkSelection
}
return rocqLightSelection
case theme.ColorNameSeparator:
return rocqSeparator
if dark {
return rocqDarkSeparator
}
return rocqLightSeparator
case theme.ColorNameDisabled:
return rocqMutedText
case theme.ColorNameSuccess:
return rocqSuccess
case theme.ColorNameError:
return rocqError
if dark {
return rocqDarkDisabled
}
return rocqLightDisabled
}
return t.base.Color(name, variant)
}
Expand Down
Loading