Jenga na Uendeshe Open Math Harness: Mafunzo ya Kivitendo ya Nucleus

Open Math Harness ni Nini?

Open Math Harness ni runtime ya chanzo huria iliyo nyuma ya Open Math OS. Kizazi chake cha kwanza, kilichoitwa Nucleus, kimeandikwa kwa Rust na kina kernel, huduma, na mawakala wanaotumiwa na jukwaa.

Runtime hii imeundwa kwa utafiti shirikishi wa hisabati. Inaweza kusaidia mawakala wanaoendesha miundo yenye uzani unaopatikana hadharani, uchunguzi sambamba wa matatizo kupitia Ultramath, utafutaji wa uthibitisho unaothibitishwa na Lean, kumbukumbu ya miradi, zana, na idhini ya binadamu kwa vitendo vilivyolindwa.

Kikomo cha sasa: runtime kamili inategemea mazingira ya uwekaji ya Open Math OS. Hifadhi inaweza kujengwa kutoka kwenye msimbo chanzo na ina mfano mdogo unaojitegemea, lakini bado haitoi mazingira ya pekee ya ndani kwa mawakala shirikishi, Ultramath, kumbukumbu, au utafutaji wa uthibitisho.

Muundo na Vipengele Vikuu

Udhibiti kwa Msingi wa Uwezo

Open Math Harness hutumia microkernel inayotegemea uwezo. Kila mchakato hupokea mamlaka iliyopewa na muundo wake pekee, na mchakato wowote unaouanzisha haupokei mamlaka zaidi ya yale ambayo mzazi unaweza kukabidhi. Hili linawahusu mawakala pamoja na programu nyingine.

Majibu ya miundo, matokeo ya zana, faili za hifadhi, na maandishi mengine huchukuliwa kuwa ingizo lisiloaminika. Maandishi hayawezi kutoa ruhusa, kuidhinisha vitendo vilivyolindwa, au kuamua ikiwa uthibitisho ni sahihi. Sifa za siri hubaki ndani ya watoa huduma wenye upendeleo finyu badala ya kufichuliwa kwa miundo, nakala za mazungumzo, au kumbukumbu.

Mawakala na Zana za Utafiti

• Mawakala wa miundo huria: Vipindi vinaweza kutumia miundo yenye uzani unaopatikana hadharani, ikiwa na majibu ya kutiririshwa, zana, mawakala wasaidizi, na historia endelevu.
• Ultramath: Mawakala wengi huchunguza kwa wakati mmoja njia tofauti za kutatua tatizo gumu, hushirikiana matokeo, na kuwasilisha ripoti kwa wakala mratibu.
• Utafutaji wa uthibitisho: Wafanyakazi huchunguza matawi katika mti wa uthibitisho wa Lean unaowezekana. Uthibitisho unaowezekana hufaulu tu ikiwa Lean itauthibitisha dhidi ya kauli asili.
• Zana za mradi: Mawakala wanaweza kufanya kazi na faili za hifadhi, shell, zana za wavuti na PDF, ujuzi wa mradi, seva za MCP, na programu-jalizi.
• Udhibiti wa binadamu: Vitendo vilivyolindwa husubiri idhini, huku rekodi za vipindi zikichanganuliwa kutafuta siri kabla ya kuonyeshwa.

Kumbukumbu ya Mradi

Kumbukumbu hudumishwa kando kwa kila mradi. Baada ya kipindi kutulia, huduma ya kumbukumbu inaweza kutoa nyenzo muhimu kutoka kwenye historia yake na kuunganisha taarifa zilizochaguliwa katika MEMORY.md. Vipindi vya baadaye hupokea kumbukumbu hii kama muktadha na hutaja nyenzo vinavyotumia.

Kumbukumbu hutoa muktadha pekee. Haiwezi kutoa ruhusa au kupuuza maagizo ya sasa ya mtumiaji.

Mahitaji ya Awali

Kabla ya kujenga Open Math Harness, andaa mazingira ya Linux yanayoungwa mkono yenye vitegemezi vifuatavyo:

• Linux: Windows na macOS hazitumiki kama wapangishaji asili wa runtime.
• Zana asili za ujenzi: Sakinisha kikusanyaji cha C na linker kwa vitegemezi asili.
• Rust kupitia rustup: Hifadhi ya msimbo hutumia rust-toolchain.toml kubainisha toolchain inayohitajika na inajumuisha vipengele vya uumbizaji na ukaguzi wa lint.
• bubblewrap: Sakinisha bwrap, iweke kwenye PATH, na uhakikishe kuwa mwenyeji anaruhusu nafasi za majina za watumiaji wasio na upendeleo.

Udhibiti ni wa lazima. Ikiwa bubblewrap haiwezi kuunda sandbox yake kwa sababu ya sera ya usalama ya mwenyeji, runtime itashindwa kuanza.

Jenga Open Math Harness kutoka kwenye Msimbo Chanzo

Clone hifadhi, ingia kwenye saraka yake, na ujenge workspace kamili ya Rust:

git clone https://github.com/openmathmodel/open-math-harness.git
cd open-math-harness
cargo build --locked --workspace

Chaguo la --locked huifanya Cargo itumie matoleo ya vitegemezi yaliyorekodiwa kwenye lockfile. Baada ya ujenzi kufanikiwa, binary za launcher na huduma zinapatikana chini ya target/debug/.

Faili zilizo chini ya deploy/vm/ zinalenga mashine pepe inayosimamiwa ya Open Math OS. Si kisakinishi cha pekee kwa kompyuta binafsi.

Endesha Mfano wa Kipande Una theJitegemea

Hifadhi ina mfano unaoendeshwa kwa hati chini ya examples/slice/. Huanzisha wakala, mfanyakazi, na huduma ya mfumo wa faili ili kuonyesha ukaguzi na ukabidhi wa uwezo.

Mfano huu hauwasiliani na mtoa huduma wa modeli na hauhitaji vitambulisho vya modeli au uwekaji wa Open Math OS. Pia hauanzishi mazungumzo shirikishi, Ultramath, kumbukumbu, au utafutaji wa uthibitisho. Linux na udhibiti unaofanya kazi wa bubblewrap bado vinahitajika.

Hatua ya 1: Anzisha Mfano

Kutoka kwenye mzizi wa hifadhi, endesha:

cargo run --locked --manifest-path cli/Cargo.toml -- run examples/slice/config.json

Hatua ya 2: Elewa Onyesho

Wakati wa uendeshaji, wakala aliyeandikwa kwa hati hufanya aina tatu muhimu za shughuli:

1. Husoma faili ambazo uwezo aliopewa unamruhusu kufikia.
2. Hukabidhi mfanyakazi wake ufikiaji wa saraka ndogo.
3. Hujaribu shughuli ambazo kernel hukataa kwa sababu zinazidi mamlaka yake.

Hili linaifanya mifano ya kipande kuwa onyesho fupi la kanuni kuu ya mradi: mchakato unaweza kutumia na kukabidhi tu uwezo ambao unamiliki kweli.

Hatua ya 3: Kagua Matokeo

Baada ya uendeshaji, kagua nakala za mazungumzo za wakala na mfanyakazi:

examples/slice/out/agent/transcript.jsonl
examples/slice/out/agent/worker/transcript.jsonl

Huduma ya mfumo wa faili hurekodi kando miito inayopokea:

examples/slice/log/access.jsonl

Mfano huu pia huunda ripoti hii:

examples/slice/data/work/report.txt

Linganisha nakala za mazungumzo na kumbukumbu ya ufikiaji wa mfumo wa faili ili kuona ni shughuli zipi ziliombwa, zilikabidhiwa, zilikubaliwa au zilikataliwa.

Endesha Mfano Tena

report.txt inayozalishwa huathiri uendeshaji unaorudiwa. Ifute kabla ya kuendesha mfano tena ikiwa unataka uundaji wa ripoti ufanikiwe tena:

rm examples/slice/data/work/report.txt
cargo run --locked --manifest-path cli/Cargo.toml -- run examples/slice/config.json

Kuhifadhi nakala za zamani za mazungumzo na faili za kumbukumbu bado kunaweza kuwa na manufaa unapolinganisha tabia kati ya uendeshaji, hivyo kagua saraka za matokeo kabla ya kufuta vizalia vingine.

Endesha Seti ya Majaribio

Baada ya kuunda workspace, endesha majaribio chaguomsingi ya Rust kutoka mzizi wa hifadhi:

cargo test --workspace

Seti chaguomsingi ya majaribio haihitaji API za modeli zinazolipiwa au vitambulisho vya uzalishaji. Baadhi ya majaribio ya ujumuishaji huanzisha michakato halisi ya watoto na kutumia bubblewrap, hivyo mahitaji yale yale ya uzuiaji wa Linux yanatumika.

Majaribio yanayohitaji watoa huduma wa modeli wa nje au usakinishaji wa Lean yamewekwa kuwa ya hiari kwa uwazi. Mtiririko wa CI wa hifadhi pia huainisha ukaguzi wa uumbizaji, Clippy, zana za Python na ukaguzi wa ujumuishaji wa MCP wa Node.js.

Matumizi ya Juu na Vidokezo vya Maendeleo

Tumia Kumbukumbu Kuchunguza Mipaka ya Uwezo

Mfano wa slice huwa na manufaa zaidi faili zake za JSON Lines zinapotumiwa kama kumbukumbu ya ukaguzi. Kagua pamoja nakala ya mazungumzo ya wakala, nakala ya mazungumzo ya mfanyakazi na kumbukumbu ya ufikiaji wa mfumo wa faili. Hii hufichua jinsi ufikiaji uliokabidhiwa unavyokuwa finyu zaidi na jinsi kernel inavyokataa shughuli zilizo nje ya mamlaka iliyotolewa.

Weka Mahitaji ya Usambazaji Tofauti

Kuunda workspace hakuzalishi kiotomatiki usakinishaji kamili wa ndani wa Open Math OS. Mawakala shirikishi pia huhitaji usanidi wa huduma, vitambulisho vya mtoa huduma wa modeli na mteja. Utafutaji wa uthibitisho pia huhitaji mazingira ya Lean na Mathlib yaliyosanidiwa.

Epuka kuchukulia usanidi wa VM inayodhibitiwa katika deploy/vm/ kuwa hati ya usakinishaji yenye matumizi ya jumla. Kwa sasa, hifadhi inaandika mfano wa slice kuwa onyesho la ndani linalojitosheleza na linaloungwa mkono.

Dumisha Utatuzi wa Cargo Unaoweza Kurudiwa

Tumia --locked pamoja na amri za ujenzi na uendeshaji zilizoandikwa. Hii huweka utatuzi wa utegemezi sambamba na lockfile ya hifadhi na hupunguza tofauti zisizotarajiwa kati ya mazingira.

Thibitisha Uzuiaji Mapema

Ikiwa uanzishaji unashindwa, kagua bubblewrap kabla ya kutatua matatizo ya huduma za kiwango cha juu. Thibitisha kuwa bwrap iko kwenye PATH na kwamba sera ya usalama ya mwenyeji inaruhusu nafasi za majina za watumiaji wasio na mapendeleo. Runtime haendelei kimakusudi bila uzuiaji unaohitajika.

Elewa Mpaka wa Uthibitishaji wa Uthibitisho

Katika usanifu kamili, imani ya wakala haithibitishi kuwa teoremu imethibitishwa. Uthibitisho unaopendekezwa hutathminiwa katika workspace zilizozuiwa zenye vikomo vya muda, na Lean huamua ikiwa imefaulu. Rekodi za utafutaji huhifadhi kazi ya watahiniwa ili awamu za baadaye ziweze kuendelea kutoka matawi ya awali.

Fuata Ukaguzi wa Michango

Kabla ya kupendekeza mabadiliko, kagua CONTRIBUTING.md na mtiririko wa CI wa hifadhi. Mwongozo wa michango unaeleza majaribio, ukaguzi wa AI na taarifa zinazotarajiwa katika maombi ya kuvuta.

Hitimisho

Open Math Harness hutoa msingi wa runtime unaolenga usalama kwa Open Math OS. Ingawa mazingira kamili shirikishi bado hayapatikani kama usanidi wa ndani unaojitegemea, unaweza kuunda workspace ya Nucleus, kuendesha mfano wake wa slice unaojitosheleza, kukagua utekelezaji wa uwezo na kuendesha majaribio chaguomsingi. Hatua hizi hutoa utangulizi wa vitendo wa kanuni kuu ya runtime: mawakala hupendekeza na kufanya kazi ndani ya mamlaka iliyoelezwa wazi, huku watu na wathibitishaji wanaoaminika wakibaki na udhibiti.