Hacktoberfest 2026: los issues que los mantenedores marcaron para octubre, abiertos y aptos para principiantes. Explorar issues de Hacktoberfest

non-evaluator attribute requires manual propagation across entire call chain

Abierto
  • ¿Algo no está bien?
#4,904 0 comentarios 0 reacciones 0 asignados Ver en GitHub

Nadie ha tomado este issue todavía.

Evaluación

Dificultad
5/5
Tiempo estimado
Más de una semana
Aptitud para principiantes
25/100
Tipo de issue
Error
Claridad
Bastante claro
Estado de actividad
Estancado
Stack tecnológico
haskell
Área
compilers

Línea de trabajo

Start by finding the original PR or issue that introduced the non-evaluator attribute, then survey its use outside mir-semantics, including the EXPERIMENT-no-llvm-kompile-updated branch. Trace how the Haskell backend sends call chains and requires clauses to the LLVM backend; done means identifying the root cause, choosing a solution direction, and implementing and verifying it.

Escrito por el modelo de indexación a partir del texto del issue.

Descripción

area:haskell-backend area:llvm-backend priority:p2 status:icebox type:feature

Problem

The non-evaluator attribute marks a function so it is not evaluated by the LLVM backend. However, in practice, marking a single function as non-evaluator is not enough — every function in the call chain above it must also be manually marked, otherwise the Haskell backend will still send the caller to the LLVM backend, which then encounters a non-evaluator function it cannot handle.

Example:

syntax Int ::= A(Int) [function, non-evaluator]
syntax Int ::= B(Int) [function]

rule B(X) => A(X) +Int 1
  • A is marked non-evaluator
  • B is not marked non-evaluator
  • When the Haskell backend simplifies B(42), since B is not non-evaluator, it sends B(42) to the LLVM backend
  • The LLVM backend attempts to evaluate, unfolds the rule, and encounters A(42) — but A is non-evaluator and the LLVM backend cannot handle it correctly
  • Workaround: manually add non-evaluator to B as well. But then all callers of B also need it, and so on — propagating up the entire call chain

The same issue occurs when a requires clause references a non-evaluator function.

This was discovered in the mir-semantics project (EXPERIMENT-no-llvm-kompile-updated branch), which has many functions unsuitable for LLVM backend execution.

Expected Behavior

non-evaluator should not require manual propagation. Possible directions:

  • The compiler automatically analyzes the call graph and propagates the attribute
  • The Haskell backend recognizes when a term contains non-evaluator functions and handles them itself
  • The LLVM backend gracefully returns unevaluated terms when encountering non-evaluator functions

Suggested First Steps

Before choosing a solution, some investigation is needed:

  1. Find the original PR/issue that introduced non-evaluator to understand the design intent
  2. Survey non-evaluator usage in projects other than mir-semantics — do they encounter the same propagation problem?
  3. Assess the semantics of non-evaluator in concrete execution (pure LLVM backend) scenarios (currently a potential concern, no observed issues yet)

Acceptance Criteria

  • Research non-evaluator introduction history and usage across projects
  • Identify root cause and solution direction
  • Implement and verify
Lenguaje dominante
Python
Estrellas
591
Forks
163
Sin PR fusionados en 30 d

Preparar el entorno

Primeros pasos

  1. Lee el issue completo y luego la guía de contribución del proyecto.
  2. Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
  3. Haz un fork del repositorio y trabaja en una rama.
  4. Abre un pull request que haga referencia al número del issue.

Más de runtimeverification/k

Todos los issues de runtimeverification/k

Issues similares

Más issues de Python

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.